-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 (𝐔❴↑i❵)) #W #HVW
+lemma cnx_inv_lref_pair (G) (L):
+ ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈𝐍 #i → ⊥.
+#G #L #I #K #V #i #HLK #H
+elim (lifts_total V (𝐔❨↑i❩)) #W #HVW