(* Constructions with pr_isu ************************************************)
(*** isuni_fwd_isfin *)
-lemma pr_isf_isu (f): ð\9d\90\94â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_isu (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
#f #H elim H -f
/3 width=1 by pr_isf_next, pr_isf_isi/
qed.