X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=113955f97fed1ded829ddd134b93e6afe4cb3237;hp=1b9f6af57abb1d37949acab4950ed27e743e06a8;hb=16fef762b0a81544a31b6392059d148431e984be;hpb=4c5c94487aa2bf5489371f112607f0a4c4f01a94

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1b9f6af..113955f 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -961,10 +961,13 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       destruct q.
       simpl in *.
       apply n.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod; auto.
-  Defined.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod.
+      apply IHX1.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
+      apply IHX2.
+      Defined.
 
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
@@ -1015,10 +1018,14 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
-    eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod; auto.
-    Defined.
+
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod.
+      apply q.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
+      apply pf.
+      Defined.
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,