-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/