Theorem: not_not (SetTheory/Formula.lean)

State before:
V : Type ?u.5243
inst✝ : SetTheory V
p : Prop
⊢ ¬¬p ↔ p
Tactic:
by_cases p <;> aesop
State after:
no goals