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

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