case not_ phi phi_ih =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
no goals