-(*
-theorem tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ≫ T → ∀T2. L ⊢ T [d, e] ≫ T2 →
- L ⊢ T1 [d, e] ≫ T2.
-#L #T1 #T #d #e #H elim H -L T1 T d e
-[ //
-| //
-| #L #K #V #V1 #V2 #i #d #e #Hdi #Hide #HLK #_ #HV12 #IHV12 #T2 #HVT2
- lapply (drop_fwd_drop2 … HLK) #H
- elim (tps_inv_lift1_up … HVT2 … H … HV12 ? ? ?) -HVT2 H HV12 // normalize [2: /2/ ] #V #HV1 #HVT2
- @tps_subst [4,5,6,8: // |1,2,3: skip | /2/ ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (tps_inv_bind1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X;
- @tps_bind /2/ @IHT12 @(tps_leq_repl … HT2) /2/
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (tps_inv_flat1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
-]
-qed.
-*)
-
-axiom tps_conf_subst_subst_lt: ∀L,K1,V1,W1,T1,i1,d,e,T2,K2,V2,W2,i2.
- ↓[O, i1] L ≡ K1. 𝕓{Abbr} V1 → ↓[O, i2] L≡ K2. 𝕓{Abbr} V2 →
- K1 ⊢ V1 [O, d + e - i1 - 1] ≫ W1 → K2 ⊢ V2 [O, d + e - i2 - 1] ≫ W2 →
- ↑[O, i1 + 1] W1 ≡ T1 → ↑[O, i2 + 1] W2 ≡ T2 →
- d ≤ i1 → i1 < d + e → d ≤ i2 → i2 < d + e → i1 < i2 →
- ∃∃T. L ⊢ T1 [d, e] ≫ T & L ⊢ T2 [d, e] ≫ T.
-(*
-#L #K1 #V1 #W1 #T1 #i1 #d #e #T2 #K2 #V2 #W2 #i2
-#HLK1 #HLK2 #HVW1 #HVW2 #HWT1 #HWT2 #Hdi1 #Hi1de #Hdi2 #Hi2de #Hi12
-*)