apply T_14_9_Deduct P U (Δ.image (evalPrimeFfToNot V))
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ) P
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P

case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P