unfold Function.updateITE
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✝)
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else evalPrimeFfToNot V (def_ a✝¹ a✝)