(* Constructions with pr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
/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« → 𝐮❨𝟎❩ ≡ f.
+lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© → 𝐮❨𝟎❩ ≡ f.
/2 width=1 by pr_isi_inv_eq_id/ qed-.