simp only [evalPrimeFfToNot_of_function_updateIte_false U' U V h1_Δ]
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U false) U' = evalPrimeFfToNot V U'
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U'.not_ U' = evalPrimeFfToNot V U'