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