Theorem: HTPI.not_and_not_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