(* Inversions with pr_uni ***************************************************)
(*** uni_isuni *)
-lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89¡ f.
+lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89\90 f.
#f #H elim H -f
[ /3 width=2 by pr_isi_inv_uni, ex_intro/
| #f #_ #g #H * /3 width=6 by pr_eq_next, ex_intro/