intro V
case h2
P : Formula
h1 : P.IsTautoPrime
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
case h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P