--- a/system-f.agda	Thu Mar 20 10:23:54 2014 +0700
+++ b/system-f.agda	Thu Mar 20 11:32:47 2014 +0700
@@ -24,16 +24,16 @@
 postulate V : Set l
 
 
-Bool = {X : Set l} -> X -> X -> X
+Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
 
-T : Bool
-T = \{X : Set l} -> \(x y : X) -> x
+T : {l : Level} -> Bool
+T {l} = \{X : Set l} -> \(x y : X) -> x
 
-F : Bool
-F = \{X : Set l} -> \(x y : X) -> y
+F : {l : Level} -> Bool
+F {l}  = \{X : Set l} -> \(x y : X) -> y
 
-D : {U : Set l} -> U -> U -> Bool -> U
-D {U} u v t = t {U} u v
+D : {l : Level} -> {U : Set l} -> U -> U -> Bool -> U
+D {l} {U} u v t = t {U} u v
 
 lemma04 : {u v : U} -> D u v T ≡  u
 lemma04 = refl
@@ -168,6 +168,39 @@
 -- 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
 
 
+List = \{l : Level} -> \{ U X : Set l}  -> X -> ( U -> X ->  X ) -> X
 
+Nil : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {X}
+Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x
+
+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 = Nil
+
+l1 : {l : Level} {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 = Cons n2 l1
 
+ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W
+ListIt {l} {U} {W} {X} w f t = t w f
 
+Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {l}} -> Bool
+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} -> List {l} {U} {X} -> List {l} {U} {X}
+Append {l} {U} {X} x y = ListIt {l} {U} {_} {X} y (\u w -> Cons u w) x
+
+Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X
+
+NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X}
+NilTree {l} {U} {X} = \(x : X) -> \(y : (U -> X) -> X) -> x
+
+Collect : {l : Level} {U : Set l} {X : Set l} -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree {l} {U} {X}
+Collect {l} {U} {X} f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )
+
+TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree {l} {U} {W} -> W
+TreeIt {l} {U} {W} {X} w h t = t w h