prove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!)

[coq-hetmet.git] / src / HaskProofToStrong.v

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 52f2154..3aee219 100644 (file)
--- 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.