simp at h2
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : IsDeduct ∅ P
⊢ IsDeduct ∅ P