proposition: Lemma nt_bounded {ff:falsity_flag} n phi : bounded n phi -> bounded n (negative_translation phi).
proof: Proof. induction 1; cbn. - solve_bounds. now econstructor. - destruct binop. now solve_bounds. - destruct quantop. now solve_bounds. - solve_bounds. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts