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