-lemma rsx_fwd_lref_pair (h) (G):
- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
- â\88\80I,K,V. â¬\87*[i] L â\89\98 K.â\93\91{I}V â\86\92 G â\8a¢ â¬\88*[h,V] ð\9d\90\92â¦\83Kâ¦\84.
-#h #G #L #i #HL #I #K #V #HLK
+lemma rsx_fwd_lref_pair_drops (G):
+ ∀L,i. G ⊢ ⬈*𝐒[#i] L →
+ â\88\80I,K,V. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 G â\8a¢ â¬\88*ð\9d\90\92[V] K.
+#G #L #i #HL #I #K #V #HLK