- â\88\80K,V,i. â¬\87*[i] L ≘ K.ⓛV → ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃#i⦄.
+ â\88\80K,V,i. â\87©*[i] L ≘ K.ⓛV → ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃#i⦄.
- â\88\80K,V,i. â¬\87*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃#i⦄ → ⊥.
+ â\88\80K,V,i. â\87©*[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