Theorem: ClassicalPropositionalLogic.isTrue_neg (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v ~A ↔ ¬IsTrue v A
Tactic:
simp
State after:
no goals