proposition: Lemma sep_eqclass P X : eqclass (sep' P X).
proof: Proof. Proof using ce. destruct (classof_ex X) as [s ->]. exists (Asep (empred P) s). apply ce. intros t. split; intros H. - destruct H as [s'[H1 H2]]; simpl in H1. now rewrite H2, (Asep_proper (@empred_Aeq P) H1). - exists s. auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)