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