X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=b14a53e8f23ca3e84921e9a1d126b599c52b70eb;hp=52f2154baa02382b6a3fe9394e9c657088e4bb0a;hb=dac68fdf6d495ed60d3e4c5738c27ca7fffc1399;hpb=9e7ea73d3a6f4bbfba279164a806490cf95efec4

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 52f2154..b14a53e 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -569,7 +569,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -715,6 +714,7 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
     rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.