--- a/system-f.agda	Sun Mar 16 21:48:15 2014 +0700
+++ b/system-f.agda	Mon Mar 17 20:10:37 2014 +0700
@@ -67,16 +67,20 @@
 
 -- Emp definision is still wrong...
 
-Emp  =  \{X : Set l } -> X
+Emp  :  {l : Level} (X : Set l) ->  Set l
+Emp {l}  =  \(X : Set l) -> X
 
-ε :  {X : Set l} -> ( {Z : Set l } -> X ) ->  Emp  {X}
-ε {U} t = t {U}
+ε :  {l l' : Level} (U : Set l)  ->  ((X : Set l) -> Emp  X) -> Emp  U
+ε U t =  t U
 
-lemma09 : {U : Set l} -> {t :  U}  -> ε {U} (ε {Emp} t)   ≡ ε {U} t
+lemma09 : {U : Set l} -> {t :  (X' : Set l) -> Emp  U}  -> ε U (ε Emp t)  ≡ ε U t
 lemma09 = refl
 
-lemma10 : {U V : Set l} -> (t :  U ×  V )  -> π1 ( ε  { U ×  V } t )  ≡ ε {U} t
-lemma10 = ?
+lemma10 : {U V : Set l} -> {t :  U ×  V }  -> π1 ( ε ( U ×  V ) {!!} )  ≡ ε U {!!}
+lemma10 = refl
+
+-- lemma101 : {U V : Set l} -> {t :  U ×  V }  -> π2 ( ε {_} { U ×  V } t )  ≡ ε {_} {V} t
+-- lemma101 = refl
 
 _+_  : Set l -> Set l -> Set (suc l)
 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X