case pred_3_ h1_v h1_phi h1_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_3_
  exact h1_1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsDeduct ∅ (h1_phi.imp_ (forall_ h1_v h1_phi))
no goals