proposition: Lemma prv_to_min_power { p : peirce } : binZF ⊢ rm_const_fm ax_power.
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. prv_all' z. repeat simpl_ex. apply II. repeat simpl_ex. apply imps. apply (AllE z) in H2. cbn in H2. now subsimpl_in H2. - assert (HP : binZF ⊢ ax_power') by (apply Ctx; firstorder). 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. + simpl_ex. apply Ctx. auto. + assert2 H. apply (AllE y) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). clear H. prv_all' z. apply II. assert2 H. apply (AllE z) in H. cbn in H. subsimpl_in H. repeat simpl_ex_in H. rewrite imps in H. repeat simpl_ex_in H. apply (Weak H). auto 8. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Asimpl Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets(binZF ZF) Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation) Morphisms Undecidability.FOL(Reductions.PCPb_to_ZFeq)