proposition: Lemma bunion_swap x y z : HFeq ⊢ (x ∪ y) ∪ z ≡ (x ∪ z) ∪ y.
proof: Proof. apply HF_ext'; auto; prv_all u; apply II. - eapply DE. eapply HF_bunion_inv; auto. + eapply DE. eapply HF_bunion_inv; auto. * apply HF_bunion_el1, HF_bunion_el1. all: auto. * apply HF_bunion_el2; auto. + apply HF_bunion_el1, HF_bunion_el2. all: auto. - eapply DE. eapply HF_bunion_inv; auto. + eapply DE. eapply HF_bunion_inv; auto. * apply HF_bunion_el1, HF_bunion_el1. all: auto. * apply HF_bunion_el2; auto. + apply HF_bunion_el1, HF_bunion_el2. all: auto. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_HF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)