case pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1 =>
  apply IsDeduct.axiom_
  exact IsAxiom.pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsDeduct ∅ ((forall_ h1_v h1_phi).imp_ h1_phi')
no goals