apply Δ_U_2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ IsDeduct ∅ P
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ Δ_U ⊆ P.primeSet

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P