proposition: Lemma nt_correct_theory T phi: (tmap negative_translation T) ⊢TI negative_translation phi -> T ⊢TC phi.
proof: Proof. intros (? & (A & -> & HA1) % tmap_contains_L & HA2 % nt_correct). now exists A. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts