-lemma rsx_sort (h) (G): āL,s. G ā¢ ā¬*[h,ās] šā¦Lā¦.
-#h #G #L1 #s @rsx_intro #L2 #H #Hs
-elim Hs -Hs /3 width=3 by lpx_fwd_length, rdeq_sort_length/
+lemma rsx_sort (G): āL,s. G ā¢ ā¬*š[ās] L.
+#G #L1 #s @rsx_intro #L2 #H #Hs
+elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_sort_length/