proposition: Lemma DN_into {p:peirce} A phi: A ⊢ phi -> A ⊢ (¬ (¬ phi)).
proof: Proof. intros H. apply II. eapply IE. 1: apply Ctx; now left. eapply Weak; [apply H|]. firstorder. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts