--- a/int.agda	Tue Apr 29 17:28:26 2014 +0900
+++ b/int.agda	Tue Apr 29 22:27:25 2014 +0900
@@ -43,7 +43,7 @@
 add {l} {U} a b = \(x : U) -> \(y : (U -> U)) -> a (b x y) y
 
 add-r : {l : Level} {U : Set l} -> Int -> Int -> Int {{!!}} {{!!}}
-add-r {l} {U} a b = (R (R O (\x -> \_ -> S x) a) (\x -> \_ -> S x) b)
+add-r {l} {U} a b = \z -> \s -> (R (R z (\x -> \_ -> s x) a) (\x -> \_ -> s x) b)
 
 lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {_} {U}
 lemma-same-add = refl

--- a/systemF.agda	Tue Apr 29 17:28:26 2014 +0900
+++ b/systemF.agda	Tue Apr 29 22:27:25 2014 +0900
@@ -45,6 +45,9 @@
 lemma-product-pi2 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
 lemma-product-pi2 = refl
 
+lemma-product-rebuild : {l : Level} {U V X : Set l} {u : U} {v : V} -> < π1 < u , v > , π2 < u , v > > {X} ≡ < u , v > {X}
+lemma-product-rebuild = refl
+
 -- Empty
 
 
@@ -117,9 +120,8 @@
 g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int)
 g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
 
--- cannot prove general Int
--- 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
+lemma-it-n : {l : Level} {U X : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> (g {l} {U} {f} < u , n >) ≡ < f u n , S n > {X}
+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 {_} {_} {f}) t)
@@ -131,7 +133,7 @@
 lemma-R-n = refl
 
 -- Proofs And Types Style lemma-R-n
--- 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
+--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
 -- n in (S n) and (R u f n) has (U × Int), but last n has Int.
 -- regenerate same (n : Int) by used g, <_,_>
 -- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"