case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  unfold Function.updateITE
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  split_ifs <;> tauto
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝) (def_ a✝¹ a✝)
no goals