+
+theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2
+@(preds_step_sn … IHM2) -M2 /2 width=2/
+qed.
+
+lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M1 -M2 /2 width=2/
+[ #A1 #A2 #_ * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+qed-.
+
+theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M2 /2 width=2/
+#M #M2 #_ #HM2 * #r #HM1
+elim (pred_lsreds … HM2) -HM2 #s #HM2
+lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
+qed-.
+
+theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
+ ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
+#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
+lapply (lsreds_preds … HM01) -s1 #HM01
+lapply (lsreds_preds … HM02) -s2 #HM02
+elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
+elim (preds_lsreds … HM1) -HM1
+elim (preds_lsreds … HM2) -HM2 /2 width=5/
+qed-.