-lemma rsx_lref_pair_drops (h) (G):
- ∀K,V. ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → G ⊢ ⬈*[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):
+ ∀K,V. ❪G,K❫ ⊢ ⬈*𝐒 V → G ⊢ ⬈*𝐒[V] K →
+ ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[#i] L.
+#G #K #V #HV #HK #I #i elim i -i