-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 â\96¼*[d, e] â\89¡ â\93\91{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
+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