-lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
- L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
+lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ U2 →
+ ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 &
+ L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 &