proposition: Lemma unionAx X Z : IN Z (Sunion X) <-> exists Y, IN Y X /\ IN Z Y.
proof: Proof. split; intros H. - apply IN_Ain_p1_NS, AunionAx in H as [y[Y1 Y2]]. exists (NS y). split; auto. - destruct H as [Y[Y1 Y2]]. apply Ain_IN_p1_NS, AunionAx. exists (proj1_sig Y). split; auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms