simp only [Function.updateITE] at h3
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {Function.updateITE (evalPrimeFfToNot V) U U.not_ U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {if True then U.not_ else evalPrimeFfToNot V U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P