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