(* Constructions with pr_uni ************************************************)
(*** isfin_uni *)
-lemma pr_isf_uni (n): ð\9d\90\85â\9dªð\9d\90®â\9d¨nâ\9d©â\9d«.
+lemma pr_isf_uni (n): ð\9d\90\85â\9d¨ð\9d\90®â\9d¨nâ\9d©â\9d©.
/3 width=2 by ex_intro/ qed.