proposition: Lemma ZF_bunion_inv' x y z : ZFeq' ⊢ z ∈ x ∪ y → z ∈ x ∨ z ∈ y.
proof: Proof. assert (TU : ZFeq' ⊢ ax_union) by (apply Ctx; firstorder). unfold ax_union in TU. eapply (AllE ({x; y})), (AllE z), CE1 in TU; cbn in TU; subsimpl_in TU. rewrite imps in *. use_exists TU u. eapply DE. apply ZF_pair_el'; auto. - eapply CE1. auto. - apply DI1. eapply ZF_eq_elem; auto. + apply ZF_refl'. auto. + eapply CE2. auto. - apply DI2. eapply ZF_eq_elem; auto. + apply ZF_refl'. auto. + eapply CE2. auto. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)