proposition: Lemma PI_eq s t (H1 : N s = s) (H2 : N t = t) : s = t -> exist (fun s => N s = s) s H1 = exist (fun s => N s = s) t H2.
proof: Proof. intros XY. subst t. f_equal. apply PI. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms