1 files changed, 12 insertions, 13 deletions

diff --git a/src/Reflection/EtaWf.v b/src/Reflection/EtaWf.v
index 97da7d1d9..abfef410b 100644
--- a/src/Reflection/EtaWf.v
+++ b/src/Reflection/EtaWf.v
@@ -24,7 +24,7 @@ Section language.
     | _ => progress destruct_head' @expr
     | _ => progress invert_expr_step
     | [ |- iff _ _ ] => split
-    | [ |- wf _ _ _ ] => constructor
+    | [ |- wf _ _ ] => constructor
     | _ => progress split_iff
     | _ => rewrite eq_interp_flat_type_eta_gen by assumption
     | [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption
@@ -49,12 +49,11 @@ Section language.
                 (exprf_eta2 : forall {t} (e : exprf t), exprf t)
                 (wff_exprf_eta : forall G t e1 e2, @wff _ _ var1 var2 G t e1 e2
                                                    <-> @wff _ _ var1 var2 G t (@exprf_eta1 t e1) (@exprf_eta2 t e2)).
-        Lemma wf_expr_eta_gen {t e1 e2} G
-          : wf G
-               (expr_eta_gen eta exprf_eta1 (t:=t) e1)
+        Lemma wf_expr_eta_gen {t e1 e2}
+          : wf (expr_eta_gen eta exprf_eta1 (t:=t) e1)
                (expr_eta_gen eta exprf_eta2 (t:=t) e2)
-            <-> wf G e1 e2.
-        Proof. Admitted.
+            <-> wf e1 e2.
+        Proof. unfold expr_eta_gen; t; inversion_wf_step; t. Qed.
       End gen_type.
 
       Lemma wff_exprf_eta_gen {t e1 e2} G
@@ -62,7 +61,7 @@ Section language.
           <-> @wff base_type_code op var1 var2 G t e1 e2.
       Proof.
         revert G; induction e1; first [ progress invert_expr | destruct e2 ];
-          t; inversion_wff_step; t.
+          t; inversion_wf_step; t.
       Qed.
     End gen_flat_type.
 
@@ -77,16 +76,16 @@ Section language.
       : wff G (exprf_eta' (t:=t) e1) (exprf_eta' (t:=t) e2)
         <-> @wff base_type_code op var1 var2 G t e1 e2.
     Proof. setoid_rewrite wff_exprf_eta_gen; intuition. Qed.
-    Lemma wf_expr_eta {t e1 e2} G
-      : wf G (expr_eta (t:=t) e1) (expr_eta (t:=t) e2)
-        <-> @wf base_type_code op var1 var2 G t e1 e2.
+    Lemma wf_expr_eta {t e1 e2}
+      : wf (expr_eta (t:=t) e1) (expr_eta (t:=t) e2)
+        <-> @wf base_type_code op var1 var2 t e1 e2.
     Proof.
       unfold expr_eta, exprf_eta.
       setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto).
     Qed.
-    Lemma wf_expr_eta' {t e1 e2} G
-      : wf G (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2)
-        <-> @wf base_type_code op var1 var2 G t e1 e2.
+    Lemma wf_expr_eta' {t e1 e2}
+      : wf (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2)
+        <-> @wf base_type_code op var1 var2 t e1 e2.
     Proof.
       unfold expr_eta', exprf_eta'.
       setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto).