apply propCompleteAux P P.primeSet
P : Formula
h1 : P.IsTautoPrime
⊢ IsDeduct ∅ P
case h1
P : Formula
h1 : P.IsTautoPrime
⊢ P.primeSet ⊆ P.primeSet

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