apply IsProofAlt.pred_1_
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt ((forall_ h1_1_v (h1_1_phi.imp_ h1_1_psi)).imp_ ((forall_ h1_1_v h1_1_phi).imp_ (forall_ h1_1_v h1_1_psi)))
no goals