proposition: Lemma PE (P P' : Prop) : (P <-> P') -> P = P'.
proof: Proof. Proof using ce. intros H. change ((fun _ : Acz => P) AEmpty = P'). now rewrite (@ce (fun _ => P) (fun _ => P')). Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)