--- a/system-f.agda	Sun Mar 16 21:33:25 2014 +0700
+++ b/system-f.agda	Sun Mar 16 21:48:15 2014 +0700
@@ -69,14 +69,14 @@
 
 Emp  =  \{X : Set l } -> X
 
-ε :  {X : Set l } -> ( Set l -> X ) ->  Emp  {X}
-ε {U} t = t U
+ε :  {X : Set l} -> ( {Z : Set l } -> X ) ->  Emp  {X}
+ε {U} t = t {U}
 
---lemma09 : {U : Set l} -> {t :  U }  -> ε {U} (ε {Emp} t)   ≡ ε {U} t
---lemma09 = ?
+lemma09 : {U : Set l} -> {t :  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 } t )  ≡ ε {U} t
+lemma10 = ?
 
 _+_  : Set l -> Set l -> Set (suc l)
 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X