proposition: Lemma sepAx P X Y : IN Y (Ssep P X) <-> IN Y X /\ P Y.
proof: Proof. Proof with try apply empred_Aeq. split; intros H. - apply IN_Ain_p1_NS, AsepAx in H as [H1 H2]... split; auto. unfold empred in H2. now rewrite NS_p1_eq in H2. - destruct H as [H1 H2]. apply Ain_IN_p1_NS, AsepAx... split; trivial. unfold empred. now rewrite NS_p1_eq. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms