case pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2 =>
  apply IsProofAlt.pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2
F h1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_phi h1_1_1 : Formula
h1_1_ih_1 : fastAdmits h1_1_v h1_1_t h1_1_phi
h1_1_ih_2 : fastReplaceFree h1_1_v h1_1_t h1_1_phi = h1_1_1
⊢ IsProofAlt ((forall_ h1_1_v h1_1_phi).imp_ h1_1_1)
no goals