proposition: Lemma ZF_bunion_el' T x y z : ZFeq' <<= T -> T ⊢ (z ∈ x ∨ z ∈ y) -> T ⊢ z ∈ x ∪ y.
proof: Proof. intros HT H. apply (DE H). - eapply ZF_union_el' with x. auto. apply CI; auto. apply ZF_pair_el'. auto. apply DI1. apply ZF_refl'. auto. - eapply ZF_union_el' with y. auto. apply CI; auto. apply ZF_pair_el'. auto. apply DI2. apply ZF_refl'. 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)