∧∧ ⦃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⦄ →
∧∧ ⦃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⦄ →