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