#h #G #L1 #s @rsx_intro #L2 #H #Hs
elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_sort_length/
qed.
(* Basic_2A1: uses: lsx_gref *)
#h #G #L1 #s @rsx_intro #L2 #H #Hs
elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_sort_length/
qed.
(* Basic_2A1: uses: lsx_gref *)