--- a/system-f.agda	Sat Mar 22 08:53:02 2014 +0700
+++ b/system-f.agda	Sat Mar 22 09:28:33 2014 +0700
@@ -188,13 +188,13 @@
 Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {U} {X}
 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )
 
-l0 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
+l0 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
 l0 = Nil
 
-l1 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
+l1 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
 l1 = Cons n1 Nil
 
-l2 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
+l2 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
 l2 = Cons n2 l1
 
 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W
@@ -204,10 +204,10 @@
 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list
 
 Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
-Append {l} {U} {X} x y = ListIt {l} {U} {_} {X} y (\u w -> Cons u w) x
+Append {l} {U} {X} x y = \s t -> x (y s t) t
 
--- lemma18 : Append l1 l2 ≡ Cons n1 ( Cons n2 Nil )
--- lemma18 = refl
+lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18 = refl
 
 Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X