(* Constructions with pr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f → 𝐈❨f❩.
+lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 f → 𝐈❨f❩.
/2 width=1 by pr_eq_id_isi/ qed.
(* Inversions with pr_isi ***************************************************)
(*** uni_isid isi_inv_uni *)
-lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f.
+lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 f.
/2 width=1 by pr_isi_inv_eq_id/ qed-.