-lemma rsx_fwd_lref_pair_drops (h) (G):
- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
- ∀I,K,V. ⇩*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
-#h #G #L #i #HL #I #K #V #HLK
+lemma rsx_fwd_lref_pair_drops (G):
+ ∀L,i. G ⊢ ⬈*𝐒[#i] L →
+ ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
+#G #L #i #HL #I #K #V #HLK