--- a/system-f.agda	Sat Apr 19 14:39:54 2014 +0900
+++ b/system-f.agda	Tue Apr 22 23:31:19 2014 +0900
@@ -190,7 +190,7 @@
 -- postulate lemma17 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int X →  U ) → (t : Int X ) → R u v (S t) ≡ v ( R u v t ) t
 
 List : {l : Level} (U X : Set l) → Set l
-List {l} = λ( U X : Set l)  → X → ( U → X →  X ) → X 
+List {l} = λ( U X : Set l)  → X → ( U → X → X ) → X 
 
 Nil : {l : Level} {U : Set l} {X : Set l} → List U X
 Nil {l} {U} {X} = λ(x : X) → λ(y : U → X → X) → x
@@ -210,11 +210,18 @@
 l3 : {l : Level} {X X' : Set l} → List (Int X) (X')
 l3 = Cons n3 l2
 
-ListIt : {l : Level} {U W : Set l} → (X : Set l) → W → ( U → W → W ) → List U W → W
-ListIt _ w f t = t w f
+--    λ x x₁ y → y x (y x (y x x₁))
+l4 : {l : Level} {X X' : Set l} → Int X → List (Int X) (X')
+l4 x = Cons x (Cons x (Cons x Nil))
 
--- Car : {l : Level} {U : Set l} {X : Set l} → List U _ → U  → U 
--- Car x z = ListIt z ( λ u w → u ) x
+ListIt : {l : Level} {U W : Set l} → W → ( U → W → W ) → List U W → W
+ListIt w f t = t w f
+
+LListIt : {l : Level} {U W : Set l} → List U W  → ( U → List U W → List U W ) → List U W → List U W
+LListIt {l} {U} {W} w f t = λ x y → t (w x y) (λ x' y' → (f x' (λ x'' y'' → y' )) x y )
+
+-- LBistIt : {l : Level} {U W X : Set l} → Bool X → ( U → Bool X → Bool X) → List U W → Bool X 
+-- LBistIt {l} {U} {W} {X} w f t = λ x → t ? ?
 
 -- Cdr : {l : Level} {U : Set l} {X : Set l} → List U _ →  List U X
 -- Cdr w = λ x → λ y →  w x (λ x y   →  y) 
@@ -226,24 +233,42 @@
 -- lemma182 = refl
 
 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool _
-Nullp {_} {_} {X} list = ListIt X (T X) (λ u w → (F X)) list
+Nullp {_} {_} {X} list = ListIt (T X) (λ u w → (F X)) list
+
+-- Nullp' : {l : Level} {U W : Set (suc l)} { X : Set (suc l)} → List U W  → Bool _
+-- Nullp' {_} {_} {_} {X} list = LBistIt (T X) (λ u w → (F X)) list
 
 -- bad append
 Append' : {l : Level} {U X : Set l} → List U (List U X) → List U X → List U X
-Append' {_} {_} {X} x y = ListIt X y Cons x
+Append' {_} {_} {X} x y = ListIt y Cons x    
 
 Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X
 Append x y = λ s t → x (y s t) t
 
+Append'' : {l : Level} {U X : Set l} → List U X → List U X → List U X
+Append'' {_} {_} {X} x y = LListIt y Cons x   
+
 lemma18 :{l : Level} {U : Set l} {X : Set l} → Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
+lemma18' :{l : Level} {U : Set l} {X : Set l} → Append'' {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18' = refl
+
+lemma18'' :{l : Level} {U : Set l} {X : Set l} → Append'' {_} {Int U} {X}  ≡ Append 
+lemma18'' = refl
+
 Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X
-Reverse {l} {U} {X} x = ListIt X Nil ( λ u w → Append w (Cons u Nil) ) x
+Reverse {l} {U} {X} x = ListIt Nil ( λ u w → Append w (Cons u Nil) ) x
 
 lemma19 :{l : Level} {U : Set l} {X : Set l} → Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
 lemma19 = refl
 
+Reverse' : {l : Level} {U : Set l} {X : Set l} → List U X → List U X
+Reverse' {l} {U} {X} x = LListIt Nil ( λ u w → Append w (Cons u Nil) ) x
+
+lemma19' :{l : Level} {U : Set l} {X : Set l} → Reverse' {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
+lemma19' = {!!}
+
 Tree : {l : Level} → Set l → Set l → Set l
 Tree {l} = λ( U X : Set l)  → X → ( (U → X) →  X ) → X