-lemma rsx_inv_lref_drops (h) (G):
- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
- â\88¨â\88¨ â¬\87*[â\92»,ð\9d\90\94â\9d´iâ\9dµ] L ≘ ⋆
- | â\88\83â\88\83I,K. â¬\87*[i] L â\89\98 K.â\93¤{I}
- | â\88\83â\88\83I,K,V. â¬\87*[i] L â\89\98 K.â\93\91{I}V & â¦\83G,Kâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vâ¦\84 & G â\8a¢ â¬\88*[h,V] ð\9d\90\92â¦\83Kâ¦\84.
-#h #G #L #i #H elim (drops_F_uni L i)
+lemma rsx_inv_lref_drops (G):
+ ∀L,i. G ⊢ ⬈*𝐒[#i] L →
+ â\88¨â\88¨ â\87©*[â\92»,ð\9d\90\94â\9d¨iâ\9d©] L ≘ ⋆
+ | â\88\83â\88\83I,K. â\87©[i] L â\89\98 K.â\93¤[I]
+ | â\88\83â\88\83I,K,V. â\87©[i] L â\89\98 K.â\93\91[I]V & â\9d¨G,Kâ\9d© â\8a¢ â¬\88*ð\9d\90\92 V & G â\8a¢ â¬\88*ð\9d\90\92[V] K.
+#G #L #i #H elim (drops_F_uni L i)