-lemma fsle_sort_bi: â\88\80L1,L2,s1,s2. |L1| = |L2| â\86\92 â¦\83L1,â\8b\86s1â¦\84 â\8a\86 â¦\83L2,â\8b\86s2â¦\84.
-/3 width=8 by lveq_length_eq, frees_sort, sle_refl, ex4_4_intro/ qed.
+lemma fsle_sort_bi: â\88\80L1,L2,s1,s2. |L1| = |L2| â\86\92 â\9dªL1,â\8b\86s1â\9d« â\8a\86 â\9dªL2,â\8b\86s2â\9d«.
+/3 width=8 by lveq_length_eq, frees_sort, pr_sle_refl, ex4_4_intro/ qed.