∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫.
/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
lemma rsx_inv_lref_drops (h) (G):
∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆
∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫.
/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
lemma rsx_inv_lref_drops (h) (G):
∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆