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