- ∀K,V,i. ⇩*[i] L ≘ K.ⓛV → ❪G,L❫ ⊢ ➡[h] 𝐍❪#i❫.
+ ∀K,V,i. ⇩[i] L ≘ K.ⓛV → ❪G,L❫ ⊢ ➡[h] 𝐍❪#i❫.
- ∀K,V,i. ⇩*[i] L ≘ K.ⓓV → ❪G,L❫ ⊢ ➡[h] 𝐍❪#i❫ → ⊥.
+ ∀K,V,i. ⇩[i] L ≘ K.ⓓV → ❪G,L❫ ⊢ ➡[h] 𝐍❪#i❫ → ⊥.
#h #G #L #K #V #i #HLK #H
elim (lifts_total V 𝐔❨↑i❩) #W #HVW
lapply (H W ?) -H [ /3 width=6 by cpm_delta_drops/ ] -HLK #H destruct
#h #G #L #K #V #i #HLK #H
elim (lifts_total V 𝐔❨↑i❩) #W #HVW
lapply (H W ?) -H [ /3 width=6 by cpm_delta_drops/ ] -HLK #H destruct