proposition: Lemma DN_T T phi : T ⊢TC (¬¬phi) -> T ⊢TC phi.
proof: Proof. intros (A & HT & HA). exists A. split; [apply HT|now apply DN]. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts