--- a/system-f.agda	Sat Mar 22 09:28:33 2014 +0700
+++ b/system-f.agda	Sat Mar 22 09:31:46 2014 +0700
@@ -206,7 +206,7 @@
 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 = \s t -> x (y s t) t
 
-lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
 Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X