-lemma csx_inv_lref: ∀h,o,G,L,i. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ →
- ∨∨ ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆
- | â\88\83â\88\83I,K. â¬\87*[i] L â\89¡ K.ⓤ{I}
- | â\88\83â\88\83I,K,V. â¬\87*[i] L â\89¡ K.â\93\91{I}V & â¦\83G, Kâ¦\84 â\8a¢ â¬\88*[h, o] 𝐒⦃V⦄.
-#h #o #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
+lemma csx_inv_lref: ∀h,G,L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ →
+ ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆
+ | â\88\83â\88\83I,K. â¬\87*[i] L â\89\98 K.ⓤ{I}
+ | â\88\83â\88\83I,K,V. â¬\87*[i] L â\89\98 K.â\93\91{I}V & â¦\83G,Kâ¦\84 â\8a¢ â¬\88*[h] 𝐒⦃V⦄.
+#h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/