⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2
| delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e))
| delifta_gref : ∀L,d,e,p. delifta d e L (§p) (§p)
⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2
| delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e))
| delifta_gref : ∀L,d,e,p. delifta d e L (§p) (§p)