--- a/system-f.agda	Sat Mar 22 18:34:13 2014 +0700
+++ b/system-f.agda	Sat Mar 22 18:46:51 2014 +0700
@@ -157,7 +157,7 @@
 -- lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int ->  U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
 -- lemma17 u v t = refl
 
--- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int ->  U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
+-- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X ->  U ) -> (t : Int X ) -> R u v (S t) ≡ v ( R u v t ) t
 
 List : {l : Level} (U X : Set l) -> Set l
 List {l} = \( U X : Set l)  -> X -> ( U -> X ->  X ) -> X 
@@ -186,13 +186,13 @@
 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _
 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list
 
-Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _
+Append : {l : Level} {U : Set l} {X : Set l} -> List U X -> List U X -> List U X
 Append x y = \s t -> x (y s t) t
 
 lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
-Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X
+Reverse : {l : Level} {U : Set l} {X : Set l} -> List U (List U X) -> List U X
 Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x
 
 lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))