proposition: Lemma bunion_eset x : ZFeq' ⊢ ∅ ∪ x ≡ x.
proof: Proof. apply ZF_ext'; auto; prv_all y; apply II. - eapply DE. eapply ZF_bunion_inv; auto. + apply Exp. eapply IE. eapply Weak; try apply ZF_eset. all: auto. + auto. - apply ZF_bunion_el2; 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)