(* these are superseded by confluence of cpms *)

lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 →
                          ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2.
#h #o #G #L #T1 #T2 #d2 *
#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1
lapply (lstas_mono … HT10 … HT1) #H destruct //
qed-.

(* Main properties **********************************************************)

theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 →
                       ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 →
                       ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2
lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/
qed-.