--- a/system-f.agda	Sat Mar 22 13:55:26 2014 +0700
+++ b/system-f.agda	Sat Mar 22 14:55:51 2014 +0700
@@ -121,11 +121,14 @@
 n3 : {l : Level } -> { X : Set l } -> Int X
 n3 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
 
+n4 : {l : Level } -> { X : Set l } -> Int X
+n4 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y (y x)))
+
 lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X}))  ≡ n2 
 lemma13 = refl
 
 It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U
-It u f t = t u f
+It {l} {U} 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 ) 
@@ -136,16 +139,16 @@
 mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X
 mul {l} {X} x y = It Zero (add x) y
 
-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
+-- fact : {l : Level} {X : Set l} -> Int _ -> Int X
+-- fact  {l} {X} n = R (S Zero) (λ (z : Int _) -> λ w -> mul z (S w) ) n
 
-lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n3 ≡ mul n1 ( mul n2 n3)
-lemma13' = refl
+-- lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( 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 n2 n3  ≡ mul {l} {X} n3 n2
+lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} 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