+lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
+ L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
+ ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
+#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
+[ -IH /2 width=3/
+| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ /2 width=3/
+ | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
+ ]
+| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ ]
+| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ ]