simp only [evalPrimeFfToNot]
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✝)
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_