proposition: Lemma sep_welldef P s : sep P (classof s) = classof (Asep (empred P) s).
proof: Proof. pose (t := Asep (empred P) s). apply (class_eq (s:=t) (s':=t)); trivial. exists s. auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)