proposition: Lemma nt_subst {ff:falsity_flag} phi σ : negative_translation (phi[σ]) = (negative_translation phi)[σ].
proof: Proof. induction phi as [| |?[]|?[]] in σ|-*; try easy. - cbn. now rewrite IHphi1, IHphi2. - cbn. now rewrite IHphi. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts