-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):
+ ∀I,L,K,V,i. ⇩*[i] L ≘ K.ⓑ[I]V →
+ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
+#h #G #I #L #K #V #i #HLK #Hi
+elim (lifts_total V (𝐔❨↑i❩))