case pred_1_ h1_v h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_1_
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
no goals