qed-.
fact rdsx_fwd_pair_aux (h) (o) (G): ∀L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
#h #o #G #L #H
@(rdsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
qed-.
fact rdsx_fwd_pair_aux (h) (o) (G): ∀L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
#h #o #G #L #H
@(rdsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct