Theorem: LO.Propositional.Classical.Formula.valAux_neg (Logic/Propositional/Classical/Basic/Semantics.lean)

State before:
α : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
inst✝ : DeMorgan F
v : α → F
p : Formula α
⊢ valAux v (~p) = ~valAux v p
Tactic:
induction p using rec' <;> simp[*, valAux, ←neg_eq, or_iff_not_imp_left]
State after:
no goals