--- a/system-f.agda	Sat Apr 19 00:29:39 2014 +0900
+++ b/system-f.agda	Sat Apr 19 11:34:49 2014 +0900
@@ -130,14 +130,11 @@
 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U
 It u f t = t u f
 
-R : {l : Level} { U X : Set l}   → U → ( U → Int X →  U ) → Int _ → U 
-R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
-
 ItInt : {l : Level} {X : Set l} → Int X → ( Int X → Int X ) → Int X → Int X
 ItInt {l} {X} u f t = λ z s → t (u z s) ( λ w → (f (λ z' s' → w )) z s )
 
--- RInt : {l : Level} { U : Set l}   → Int U → ( Int U → Int U →  Int U ) → Int U → Int U 
--- RInt {l} {U} u v t =  π1 ( ItInt {suc l} {Int U ×  Int U} (< u , Zero >) (λ (x : Int U × Int U) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
+R : {l : Level} { U X : Set l}   → U → ( U → Int X →  U ) → Int _ → U 
+R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
 -- bad adder which modifies input type
 add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X
@@ -146,6 +143,12 @@
 add : {l : Level} {X : Set l} → Int X → Int X → Int X
 add x y = λ z s → x (y z s) s
 
+add'' : {l : Level} {X : Set l} → Int X → Int X → Int X
+add'' x y = ItInt y S x
+
+lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y  ≡ add'' x y
+lemma22 x y = refl
+
 -- bad adder which modifies input type
 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
 mul' {l} {X} x y = It Zero (add x) y
@@ -162,6 +165,12 @@
 lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
 lemma13' = refl
 
+-- lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → mul x y  ≡ mul'' x y
+-- lemma23 x y = {!!}
+
+lemma24 :  {l : Level } {X : Set l} → mul {l} {X} n4 n3  ≡ mul'' {l} {X} n3 n4
+lemma24 = refl
+
 
 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}