--- a/system-f.agda	Tue Apr 22 23:31:19 2014 +0900
+++ b/system-f.agda	Sat May 03 11:46:05 2014 +0900
@@ -47,32 +47,38 @@
 
 -- Emp definision is still wrong...
 
-Emp  :  {l : Level} {X : Set l} →  Set l
-Emp {l} = λ{X : Set l} → X
+Emp  :  {l : Level} (U : Set l) →  Set l
+Emp {l} = λ( U : Set l) → U
+
+-- Emp is not allowed because Emp is not a Set of any level
+
+-- t : Emp
+-- t = ?
 
--- ε :  {l : Level} (U : Set l)  {l' : Level} {U' : Set l'}  → Emp → Emp 
--- ε {l} U t =  t 
+-- ε :  {l : Level} (U : Set l)  → Emp → U
+-- ε {l} U t =  t U
 
--- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} → (t : Emp {l} {U} ) → ε U (ε Emp t) ≡ ε U t
+-- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε (U → V) t) u ≡ ε V t
+-- lemma103 u t = refl
+
+-- lemma09 : {l : Level} {U : Set l}  → (t : Emp ) → ε U (ε Emp t) ≡ ε U t
 -- lemma09 t = refl
 
--- lemma10 :  {l : Level} {U V X : Set l} →  (t : Emp {_} {U ×  V}) → U × V
+-- lemma10 :  {l : Level} {U V X : Set l} →  (t : Emp ) → U × V
 -- lemma10  {l} {U} {V} t = ε (U ×  V) t
 
--- lemma10' : {l : Level} {U V X : Set l} →  (t : Emp {_} {U ×  V}) → Emp
+-- lemma10' : {l : Level} {U V X : Set l} →  (t : Emp ) → Emp
 -- lemma10' {l} {U} {V} {X} t = ε (U ×  V) t 
 
--- lemma100 : {l : Level} {U V X : Set l} →  (t : Emp {_} {U}) → Emp
+-- lemma100 : {l : Level} {U V X : Set l} →  (t : Emp ) → Emp 
 -- lemma100 {l} {U} {V} t = ε U t
 
--- lemma101 : {l k : Level} {U V : Set l} →  (t : Emp {_} {U × V}) → π1 (ε (U ×  V) t) ≡ ε U t
+-- lemma101 : {l k : Level} {U V : Set l} →  (t : Emp ) → π1 (ε (U ×  V) t) ≡ ε U t
 -- lemma101 t = refl
 
--- lemma102 : {l k : Level} {U V : Set l} →  (t : Emp {_} {U × V}) → π2 (ε (U ×  V) t) ≡ ε V t
+-- lemma102 : {l k : Level} {U V : Set l} →  (t : Emp ) → π2 (ε (U ×  V) t) ≡ ε V t
 -- lemma102 t = refl
 
--- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} {_} ) → (ε (U → V) t) u ≡ ε V t
--- lemma103 u t = refl
 
 _+_  : {l : Level} → Set l → Set l → Set (suc l)
 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X
@@ -157,7 +163,7 @@
 mul {l} {X} x y = λ z s → x z ( λ w → y w s )
 
 mul'' : {l : Level } {X : Set l} → Int X → Int X → Int X
-mul'' {l} {X} x y = ItInt Zero (add x) y
+mul'' {l} {X} x y = ItInt Zero (add'' x) y
 
 fact : {l : Level} {X : Set l} → Int _ → Int X
 fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w)) n
@@ -220,10 +226,7 @@
 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 : {l : Level} {U : Set l} {X : Set l} → List U X →  List U X
 -- Cdr w = λ x → λ y →  w x (λ x y   →  y) 
 
 -- lemma181 :{l : Level} {U : Set l} {X : Set l} → Car Zero l2 ≡ n2
@@ -232,12 +235,9 @@
 -- lemma182 :{l : Level} {U : Set l} {X : Set l} → Cdr l2 ≡ l1
 -- lemma182 = refl
 
-Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool _
+Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool X
 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 y Cons x    
@@ -259,15 +259,17 @@
 
 Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X
 Reverse {l} {U} {X} x = ListIt Nil ( λ u w → Append w (Cons u Nil) ) x
+-- λ x → x (λ x₁ y → x₁) (λ u w s t → w (t u s) t)
 
 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
+-- λ x x₁ y → x x₁ (λ x' y' → y')
 
-lemma19' :{l : Level} {U : Set l} {X : Set l} → Reverse' {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
-lemma19' = {!!}
+-- 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