induction Δ_U using Finset.induction_on
P : Formula
Δ_U : Finset Formula
h1 : Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
⊢ IsDeduct ∅ P
case empty
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P

case insert
P a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) s✝)) P) → IsDeduct ∅ P
h1 : insert a✝² s✝ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert a✝² s✝))) P
⊢ IsDeduct ∅ P