proposition: Lemma nt_dn_float {p:peirce} {ff:falsity_flag} A phi : A ⊢ (¬¬negative_translation phi) -> A ⊢ negative_translation phi.
proof: Proof. intros H. eapply IE. 1: apply nt_dn_float'. easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts