-lemma rsx_lref_pair_drops (h) (G):
- â\88\80K,V. â\9dªG,Kâ\9d« â\8a¢ â¬\88*ð\9d\90\92[h] V â\86\92 G â\8a¢ â¬\88*ð\9d\90\92[h,V] K →
- ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L.
-#h #G #K #V #HV #HK #I #i elim i -i
+lemma rsx_lref_pair_drops (G):
+ â\88\80K,V. â\9d¨G,Kâ\9d© â\8a¢ â¬\88*ð\9d\90\92 V â\86\92 G â\8a¢ â¬\88*ð\9d\90\92[V] K →
+ ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[#i] L.
+#G #K #V #HV #HK #I #i elim i -i