proposition: Lemma DN A phi: A ⊢C (¬ (¬ phi)) -> A ⊢C phi.
proof: Proof. intros H. eapply IE. 1: apply Pc. eapply II. apply Exp. eapply IE. 2: apply Ctx; now left. eapply Weak. 1: apply H. intros a Ha; now right. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts