proposition: Lemma prv_to_min_union { p : peirce } : minZFeq' ⊢ rm_const_fm ax_union.
proof: Proof. prv_all x. prv_all y. apply CI. - simpl_ex. apply II. assert1 H. use_exists' H u. clear H. assert1 H. apply CE in H as [H1 H2]. simpl_ex_in H1. apply (AllE y) in H1. cbn in H1. subsimpl_in H1. apply CE1 in H1. apply (IE H1) in H2. use_exists' H2 z. apply (ExI z). cbn. subsimpl. apply CI; repeat simpl_ex. + eapply CE1. auto. + eapply CE2. auto. - assert (HU : minZFeq' ⊢ ax_union') by (apply Ctx; firstorder). apply (AllE x) in HU. cbn in HU. use_exists' HU u. apply II. assert1 H. use_exists' H z. clear H. assert1 H. apply CE in H as [H1 H2]. repeat simpl_ex_in H1. repeat simpl_ex_in H2. simpl_ex. apply (ExI u). cbn. subsimpl. apply CI. + simpl_ex. apply Ctx. auto. + assert3 Hu. apply (AllE y) in Hu. cbn in Hu. subsimpl_in Hu. apply CE2 in Hu. apply (IE Hu). apply (ExI z). cbn. subsimpl. now apply CI. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets(minZF ZF) Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation)