-lemma csx_inv_lref_drops (h) (G):
- ∀L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ →
- â\88¨â\88¨ â\87©*[â\92»,ð\9d\90\94â\9d´iâ\9dµ] L ≘ ⋆
- | ∃∃I,K. ⇩*[i] L ≘ K.ⓤ{I}
- | ∃∃I,K,V. ⇩*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
-#h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
+lemma csx_inv_lref_drops (G) (L):
+ ∀i. ❪G,L❫ ⊢ ⬈*𝐒 #i →
+ â\88¨â\88¨ â\87©*[â\92»,ð\9d\90\94â\9d¨iâ\9d©] L ≘ ⋆
+ | ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I]
+ | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒 V.
+#G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/