proposition: Lemma sepAx P X Y : ele Y (sep P X) <-> ele Y X /\ P Y.
proof: Proof. destruct (classof_ex Y) as [s ->]. destruct (classof_ex X) as [t ->]. rewrite sep_welldef. repeat rewrite classof_ele. apply AsepAx, empred_Aeq. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)