-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, reqx_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, reqg_sort_length/