-lemma cnx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄ → ⊥.
-#h #o #I #G #L #K #V #i #HLK #H
-elim (lifts_total V (ð\9d\90\94â\9d´â\86\91iâ\9dµ)) #W #HVW
+lemma cnx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫ → ⊥.
+#h #I #G #L #K #V #i #HLK #H
+elim (lifts_total V (ð\9d\90\94â\9d¨â\86\91iâ\9d©)) #W #HVW