Theorem: HTPI.not_not_or_distrib (HTPILib/HTPIDefs.lean)

State before:
p q : Prop
⊢ ¬(¬p ∨ q) ↔ p ∧ ¬q
Tactic:
rw [not_or, Classical.not_not]
State after:
no goals