proposition: Lemma rm_const_tm_equiv { p : peirce } A t (x y : term') : minZFeq' <<= A -> A ⊢ (rm_const_tm t)[x..] -> A ⊢ y ≡' x <-> A ⊢ (rm_const_tm t)[y..].
proof: Proof. intros HA Hx. split; intros H. - eapply minZF_Leibniz; eauto. - apply minZF_ext; trivial; eapply rm_const_tm_sub; eauto. 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)