Theorem: HW2.bonus_challenge (BrownCs22/Homework/Hw2.lean)

State before:
p : Prop
⊢ ¬(p ↔ ¬p)
Tactic:
sorry
State after:
no goals