proposition: Lemma unionAx X Z : ele Z (union X) <-> exists Y, ele Y X /\ ele Z Y.
proof: Proof. destruct (classof_ex Z) as [u ->]. destruct (classof_ex X) as [s ->]. rewrite union_welldef, classof_ele, AunionAx. split; intros [t H]. - exists (classof t). now repeat rewrite classof_ele. - destruct (classof_ex t) as [t' ->]. exists t'. now repeat rewrite <- classof_ele. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)