proposition: Lemma nt_impl {ff:falsity_flag} A phi : negative_translation (impl A phi) = impl (map negative_translation A) (negative_translation phi).
proof: Proof. induction A as [|psi A IH]; cbn; congruence. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts