-lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
- ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
- d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2 width=1/ (**) (* /3 width=6/ is too slow *)
-qed.
-
-lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 →
- ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
-#L0 #L1 #d #e #H @(ltpss_ind … H) -L1
-[ /2 width=1/
-| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
- lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 -HTU2 /2 width=1/
-]
-qed.
-
-lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 →
- ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
-/3 width=3/ qed.
-
-lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
- L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶* L1 →
- L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
-[ //
-| -HTU2 #L #L1 #_ #HL1 #IHL
- lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 -IHL //
-]
-qed.
-
-lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
- L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶* L1 →
- L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
-@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2 width=1/ (**) (* /3 width=6/ is too slow *)
-qed.
-
-lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
- L0 ⊢ T2 [d, e] ▶* U2 → L0 [d, e] ▶* L1 →
- ∃∃T. L1 ⊢ T2 [d, e] ▶* T & L1 ⊢ U2 [d, e] ▶* T.
-#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
+(* Basic_1: was: subst1_subst1_back *)
+lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+ L1 ⊢ U2 ▶* [d1, e1] T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2