proposition: Lemma nt_correct A phi: (map negative_translation A) ⊢I negative_translation phi -> A ⊢C phi.
proof: Proof. intros H. apply big_imps_nil. apply nt_Cprv_equiv. eapply prv_transport_to_class. rewrite nt_impl. apply big_imps_nil in H. apply H. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts