simp only [Formula.IsTautoPrime] at h2
P Q : Formula
h2 : P.IsTautoPrime
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
P Q : Formula
h2 : ∀ (V : VarBoolAssignment), evalPrime V P
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime