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