classical.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

  Context (excl: ∀ A, A ∨ ~ A).
  Goal ∀ A, ¬¬A → A.excl:∀ A : Prop, A ∨ ¬ A
∀ A : Prop, ¬ ¬ A → A
    intros A notnot_A.excl:∀ A0 : Prop, A0 ∨ ¬ A0
A:Prop
notnot_A:¬ ¬ A
A
(λ (A : Prop) (notnot_A : ¬ ¬ A), ?Goal)    destruct (excl A) as [a | na].excl:∀ A0 : Prop, A0 ∨ ¬ A0
A:Prop
notnot_A:¬ ¬ A
a:A
A
excl:∀ A0 : Prop, A0 ∨ ¬ A0
A:Prop
notnot_A:¬ ¬ A
na:¬ A
A
(λ (A : Prop) (notnot_A : ¬ ¬ A),
   let o : A ∨ ¬ A := excl A in
   match o with
   | or_introl a => ?Goal
   | or_intror na => ?Goal0
   end)    -excl:∀ A0 : Prop, A0 ∨ ¬ A0
A:Prop
notnot_A:¬ ¬ A
a:A
A assumption.
(λ (A : Prop) (notnot_A : ¬ ¬ A),
   let o : A ∨ ¬ A := excl A in
   match o with
   | or_introl a => a
   | or_intror na => ?Goal
   end)