X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=35373a76657a4ff168a0f9f260dd2efbbdcf4cf2;hp=1b9f6af57abb1d37949acab4950ed27e743e06a8;hb=6a7c6977507488245ba4b8cabcf323920c25baef;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1b9f6af..35373a7 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 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 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,