# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1397103673 -32400
# Node ID 08b8ced4e90ec4709619f8462fcb884c627950a7
# Parent  cc34bf8772a9773d2abde82f62b7b13427365091
lemma-R

diff -r cc34bf8772a9 -r 08b8ced4e90e systemF.agda
--- a/systemF.agda	Thu Apr 10 11:34:43 2014 +0900
+++ b/systemF.agda	Thu Apr 10 13:21:13 2014 +0900
@@ -121,5 +121,11 @@
 -- lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
 -- lemma-it-n = refl
 
-R : {l : Level} -> {U : Set l} -> U -> (U → Int → U) -> Int -> U
-R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {l} {U} {f}) t)
\ No newline at end of file
+R : {l : Level} -> {U : Set l} -> U -> (U -> Int -> U) -> Int -> U
+R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {_} {_} {f}) t)
+
+lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u
+lemma-R-O = refl
+
+lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (\u n ->  π2 < u , n > ))
+lemma-R-n = refl