proposition: Lemma prv_to_min_pair { p : peirce } : minZFeq' ⊢ rm_const_fm ax_pair.
proof: Proof. prv_all x. prv_all y. prv_all z. apply CI. - simpl_ex. apply II. assert1 H. use_exists' H u. clear H. assert1 H. apply CE in H as [H1 H2]. repeat simpl_ex_in H1. apply (AllE z) in H1. cbn in H1. subsimpl_in H1. apply CE1 in H1. apply (IE H1) in H2. apply (DE H2); [apply DI1 | apply DI2]. all: repeat simpl_ex. - assert (HP : minZFeq' ⊢ ax_pair') by (apply Ctx; firstorder). apply (AllE y) in HP. cbn in HP. apply (AllE x) in HP. cbn in HP. use_exists' HP u. clear HP. apply II. simpl_ex. apply (ExI u). cbn. subsimpl. apply CI. + repeat simpl_ex. + assert2 H. apply (AllE z) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). clear H. eapply DE. * apply Ctx. auto. * apply DI1. assert1 H. repeat simpl_ex_in H. * apply DI2. assert1 H. repeat simpl_ex_in H. 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)