-lemma fsle_sort: â\88\80L,s1,s2. â\9dªL,â\8b\86s1â\9d« â\8a\86 â\9dªL,â\8b\86s2â\9d«.
-/3 width=8 by frees_sort, sle_refl, ex4_4_intro/ qed.
+lemma fsle_sort: â\88\80L,s1,s2. â\9d¨L,â\8b\86s1â\9d© â\8a\86 â\9d¨L,â\8b\86s2â\9d©.
+/3 width=8 by frees_sort, pr_sle_refl, ex4_4_intro/ qed.