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