--- a/system-f.agda	Fri Mar 21 17:30:46 2014 +0700
+++ b/system-f.agda	Sat Mar 22 08:53:02 2014 +0700
@@ -67,28 +67,31 @@
 
 -- Emp definision is still wrong...
 
-Emp  :  ∀{l : Level} {X : Set l} ->  Set l
-Emp {l}  =  \{X : Set l} -> X
+Emp  :  {l : Level} {X : Set l} ->  Set l
+Emp {l} = \{X : Set l} -> X
 
--- ε :  {l : Level} {U : Set l}  -> Emp  -> Emp 
--- ε {l} {U} t =  t {l} {U}
+-- ε :  {l : Level} (U : Set l)  {l' : Level} {U' : Set l'}  -> Emp -> Emp 
+-- ε {l} U t =  t 
 
--- lemma09 : {l : Level} {U : Set l} -> (t : Emp) -> ε U (ε Emp t) ≡ ε U t
+-- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t
 -- lemma09 t = refl
 
--- 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}) -> U × V
+-- lemma10  {l} {U} {V} t = ε (U ×  V) t
 
--- lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> Emp
+-- lemma10' : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U ×  V}) -> Emp
+-- lemma10' {l} {U} {V} {X} t = ε (U ×  V) t 
+
+-- lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U}) -> Emp
 -- lemma100 {l} {U} {V} t = ε U t
 
--- lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π1 (ε (U ×  V) t) ≡ ε U t
+-- lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π1 (ε (U ×  V) t) ≡ ε U t
 -- lemma101 t = refl
 
--- lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π2 (ε (U ×  V) t) ≡ ε V t
+-- lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π2 (ε (U ×  V) t) ≡ ε V t
 -- lemma102 t = refl
 
--- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp) -> ε (U -> V) u ≡ ε V t
+-- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
 -- lemma103 u t = refl
 
 _+_  : Set l -> Set l -> Set (suc l)