-fact ltpss_dx_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_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_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_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_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_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_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_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_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_dx_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/
- ]
-]
-qed.
-