--- a/system-f.agda	Mon Mar 17 20:10:37 2014 +0700
+++ b/system-f.agda	Mon Mar 17 21:29:45 2014 +0700
@@ -67,13 +67,13 @@
 
 -- 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 l' : Level} (U : Set l)  ->  ((X : Set l) -> Emp  X) -> Emp  U
+ε :  {l l' : Level} (U : Set l)  ->  ((X : Set l) -> Emp {l} {X}) -> Emp {l} {U}
 ε U t =  t U
 
-lemma09 : {U : Set l} -> {t :  (X' : Set l) -> Emp  U}  -> ε U (ε Emp t)  ≡ ε U t
+lemma09 : {l l' : Level} {U : Set l} -> {t :  (X' : Set (suc l)) -> Emp }  -> ε U (ε Emp t) ≡ ε U ?
 lemma09 = refl
 
 lemma10 : {U V : Set l} -> {t :  U ×  V }  -> π1 ( ε ( U ×  V ) {!!} )  ≡ ε U {!!}