(* Alternative definition of isid *******************************************)
-lemma eq_id_isid: â\88\80f. ð\9d\90\88ð\9d\90\9d â\89\97 f → 𝐈⦃f⦄.
+lemma eq_id_isid: â\88\80f. ð\9d\90\88ð\9d\90\9d â\89¡ f → 𝐈⦃f⦄.
/2 width=3 by isid_eq_repl_back/ qed.
-lemma eq_id_inv_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\88ð\9d\90\9d â\89\97 f.
+lemma eq_id_inv_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\88ð\9d\90\9d â\89¡ f.
/2 width=1 by isid_inv_eq_repl/ qed-.