(*** isuni *)
inductive pr_isu: predicate pr_map ≝
(*** isuni_isid *)
-| pr_isu_isi (f): ð\9d\90\88â\9dªfâ\9d« → pr_isu f
+| pr_isu_isi (f): ð\9d\90\88â\9d¨fâ\9d© → pr_isu f
(*** isuni_next *)
| pr_isu_next (f): pr_isu f → ∀g. ↑f = g → pr_isu g
.
(* Basic inversions *********************************************************)
(*** isuni_inv_push *)
-lemma pr_isu_inv_push (g): ð\9d\90\94â\9dªgâ\9d« â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma pr_isu_inv_push (g): ð\9d\90\94â\9d¨gâ\9d© â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
#g * -g
[ /2 width=3 by pr_isi_inv_push/
| #f #_ #g #H #x #Hx destruct
qed-.
(*** isuni_inv_next *)
-lemma pr_isu_inv_next (g): ð\9d\90\94â\9dªgâ\9d« â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\94â\9dªfâ\9d«.
+lemma pr_isu_inv_next (g): ð\9d\90\94â\9d¨gâ\9d© â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\94â\9d¨fâ\9d©.
#g * -g #f #Hf
[ #x #Hx elim (pr_isi_inv_next … Hf … Hx)
| #g #H #x #Hx destruct
(* Basic destructions *******************************************************)
(*** isuni_fwd_push *)
-lemma pr_isu_fwd_push (g): ð\9d\90\94â\9dªgâ\9d« â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\94â\9dªfâ\9d«.
+lemma pr_isu_fwd_push (g): ð\9d\90\94â\9d¨gâ\9d© â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\94â\9d¨fâ\9d©.
/3 width=3 by pr_isu_inv_push, pr_isu_isi/ qed-.