-lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
- L â\8a¢ â\93\91{I} V1. T1 [d, e] â\89¡ â\93\91{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lemma delift_bind: ∀a,I,L,V1,V2,T1,T2,d,e.
+ L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 →
+ L â\8a¢ â\96¼*[d, e] â\93\91{a,I} V1. T1 â\89¡ â\93\91{a,I} V2. T2.
+#a #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
+lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/