-lemma csx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
- ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
-#h #I #G #L #K #V #i #HLK #Hi
-elim (lifts_total V (𝐔❴↑i❵))
+lemma csx_inv_lref_pair_drops (h) (G) (L):
+ ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
+ ❪G,L❫ ⊢ ⬈*𝐒[h] #i → ❪G,K❫ ⊢ ⬈*𝐒[h] V.
+#h #G #L #I #K #V #i #HLK #Hi
+elim (lifts_total V (𝐔❨↑i❩))