--- a/systemF.agda	Thu Apr 10 14:29:37 2014 +0900
+++ b/systemF.agda	Thu Apr 10 16:26:28 2014 +0900
@@ -139,20 +139,27 @@
 
 -- List
 
-List : {l : Level} -> (U : Set l) -> Set (suc l)
-List {l} U = {X : Set l} -> X -> (U -> X -> X) -> X
+List : {l : Level} {ll : Level} -> (U : Set l) -> Set (suc ll ⊔ l)
+List {l} {ll} U = {X : Set ll} -> X -> (U -> X -> X) -> X
 
-nil : {l : Level} {U : Set l} -> List U
-nil {l} {U} = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> x
+nil : {l : Level} {ll : Level} {U : Set l} -> List U
+nil {l} {ll} {U} = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> x
 
-cons : {l : Level} {U : Set l} -> U -> List U -> List U
-cons {l} {U} u t = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
+cons : {l : Level} {ll : Level} {U : Set l} -> U -> List U -> List U
+cons {l} {ll} {U} u t = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
 
-ListIt : {l : Level} {U W : Set l} -> W -> (U -> W -> W) -> List U -> W
-ListIt {l} {U} {W} w f t = t {W} w f
+ListIt : {l : Level} {ll : Level} {U : Set l} {W : Set ll} -> W -> (U -> W -> W) -> List U -> W
+ListIt {l} {ll} {U} {W} w f t = t {W} w f
+
+-- (u1 u2 nil)
+lemma-list : {l : Level} {ll : Level} {U : Set l} {X : Set ll} {u1 u2 : U} {x : X} {y : U -> X -> X} -> (cons u1 (cons u2 nil)) x y ≡ y u1 (y u2 x)
+lemma-list = refl
 
 lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
 lemma-list-it-nil = refl
 
 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
-lemma-list-it-cons = refl
\ No newline at end of file
+lemma-list-it-cons = refl
+
+--lemma-list-nil-cons : {l : Level} {ll : Level} {U : Set l} {W : Set ll} {t : List U} -> ListIt {l} {?} {U} {List U} (nil {l} {ll} {U}) ({!!}) t ≡ t
+--lemma-list-nil-cons = {!!}
\ No newline at end of file