--- a/system-f.agda	Sat Mar 22 11:51:34 2014 +0700
+++ b/system-f.agda	Sat Mar 22 13:55:26 2014 +0700
@@ -131,24 +131,21 @@
 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 ) 
 
 add : {l : Level} {X : Set l} -> Int (Int X) -> Int X -> Int X
-add x y = It y ( λ z -> S z ) x
+add x y = It y S x
 
 mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X
-mul  x y = It Zero ( λ z -> add y z ) x
-
-copyInt : {l : Level } {X : Set l} -> Int (Int X) -> Int X
-copyInt  x = It Zero ( λ (z : Int _) -> S z ) x
+mul {l} {X} x y = It Zero (add x) y
 
-fact : {l : Level} {X : Set l} -> Int _ -> Int X
-fact  {l} {X} n = R (S Zero) (λ z -> λ w -> mul (S w) w ) n
+fact : {l : Level} {X : Set l} -> Int _ -> Int (Int X)
+fact  {l} {X} n = R (S Zero) (λ (z : Int (Int X)) -> λ w -> mul w (S w) ) n
 
--- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3)
--- lemma13' = refl
+lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n3 ≡ mul n1 ( mul n2 n3)
+lemma13' = refl
 
 -- lemma14 : (x y : Int) -> mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}
 
-lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
+lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul n2 n3  ≡ mul {l} {X} n3 n2
 lemma15 x y = refl
 
 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X ->  U ) -> R u v Zero ≡ u