Theorem: Smt.Reconstruct.Builtin.notNotElim (Smt/Reconstruct/Builtin/Lemmas.lean)

State before:
⊢ ∀ {p : Prop}, ¬¬p → p
Tactic:
intros p h
State after:
p : Prop
h : ¬¬p
⊢ p

State before:
p : Prop
h : ¬¬p
⊢ p
Tactic:
exact match Classical.em p with
| Or.inl pp => pp
| Or.inr np => False.elim (h (λ p => np p))
State after:
no goals