proposition: Lemma Peirce (P Q : Prop) : ((P -> Q) -> P) -> P.
proof: Proof. Proof using LEM. destruct (LEM (((P -> Q) -> P) -> P)); tauto. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullND Undecidability(Shared.ListAutomation) Vector Lia