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

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