proposition: Lemma nt_peirce {p:peirce} {ff:falsity_flag} A phi psi: A ⊢ negative_translation (((phi → psi) → phi) → phi).
proof: Proof. cbn. apply II. apply nt_dn_float. apply II. eapply IE. 1: apply Ctx; now left. eapply IE. 1: apply Ctx; right; now left. apply II. apply Exp. eapply IE. 1: apply Ctx; right; now left. apply Ctx. now left. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts