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

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