--- a/systemF.agda	Thu Apr 10 13:25:48 2014 +0900
+++ b/systemF.agda	Thu Apr 10 14:29:37 2014 +0900
@@ -134,6 +134,25 @@
 -- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n
 -- n in (S n) and (R u f n) has (U × Int), but last n has Int.
 -- regenerate same (n : Int) by used g, <_,_>
+-- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"
 
 
+-- List
 
+List : {l : Level} -> (U : Set l) -> Set (suc l)
+List {l} U = {X : Set l} -> 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
+
+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)
+
+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
+
+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