proposition: Lemma prv_to_min_om2 { p : peirce } : minZFeq' ⊢ rm_const_fm ax_om2.
proof: Proof. cbn. prv_all x. destruct x as [n|[]]. cbn. rewrite rm_const_fm_subst, inductive_subst, !is_inductive_subst. cbn. apply II. prv_all m. cbn. rewrite !is_inductive_subst. cbn. simpl_ex. rewrite !is_inductive_subst. cbn. apply II. simpl_ex. change (∃ $0 ≡' ↑ n ∧ m`[↑] ∈' $0) with (∃ $0 ≡' $n`[↑] ∧ m`[↑] ∈' $0). simpl_ex. assert1 H. use_exists' H k. clear H. cbn. rewrite !is_inductive_subst. cbn. subsimpl. assert1 H. apply CE in H as [H1 % CE2 H2]. apply (AllE $n) in H1. cbn in H1. subsimpl_in H1. rewrite is_inductive_subst in H1. cbn in H1. assert3 H3. apply prv_to_min_inductive in H3; auto. apply (IE H1) in H3. apply (AllE m) in H3. cbn in H3. subsimpl_in H3. now apply (IE H3). 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)