simp only [Formula.IsTautoPrime] at h1
case h2.h3
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P