cases h1
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 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
case h2.intro
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
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
left✝ : U ∈ P.primeSet
right✝ : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P