proposition: Lemma rm_const_tm_prv { p : peirce } t : binZF ⊢ ∃ rm_const_tm t.
proof: Proof. induction t; try destruct F; cbn. - apply (ExI $x). cbn. apply minZF_refl'. - apply Ctx. firstorder. - rewrite (vec_inv2 v). cbn. assert (H1 : binZF ⊢ ∃ rm_const_tm (Vector.hd v)) by apply IH, in_hd. assert (H2 : binZF ⊢ ∃ rm_const_tm (Vector.hd (Vector.tl v))) by apply IH, in_hd_tl. use_exists' H1 x. eapply Weak in H2. use_exists' H2 y. 2: auto. assert (H : binZF ⊢ ax_pair') by (apply Ctx; firstorder). apply (AllE x) in H. cbn in H. apply (AllE y) in H. cbn in H. eapply Weak in H. use_exists' H z. 2: auto. apply (ExI z). cbn. apply (ExI x). cbn. subsimpl. rewrite eq_sshift1. apply CI; auto. apply (ExI y). cbn. subsimpl. erewrite !subst_comp, subst_ext. rewrite eq_subst. cbn. subsimpl. apply CI; auto. now intros []. - rewrite (vec_inv1 v). cbn. specialize (IH _ (in_hd v)). use_exists' IH x. assert (H : binZF ⊢ ax_union') by (apply Ctx; firstorder). apply (AllE x) in H. cbn in H. eapply Weak in H. use_exists' H y. 2: auto. apply (ExI y). cbn. apply (ExI x). cbn. subsimpl. rewrite eq_sshift1. apply CI; auto. - rewrite (vec_inv1 v). cbn. specialize (IH _ (in_hd v)). use_exists' IH x. assert (H : binZF ⊢ ax_power') by (apply Ctx; firstorder). apply (AllE x) in H. cbn in H. eapply Weak in H. use_exists' H y. 2: auto. apply (ExI y). cbn. apply (ExI x). cbn. subsimpl. rewrite eq_sshift1. apply CI; auto. - apply Ctx. firstorder. 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)