X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;fp=src%2FHaskProofToStrong.v;h=3aee2197d4534b90b053b68160dbd3338141b16a;hp=52f2154baa02382b6a3fe9394e9c657088e4bb0a;hb=1cfe65d4e2d3292cc038882d8518dd7a48e2c40a;hpb=9ae7c0c0ae44417d2171487376ae66dc9eaad20a

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 52f2154..3aee219 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -715,6 +715,7 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
     rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.