apply IsProofAlt.pred_3_
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ IsProofAlt (h1_1_phi.imp_ (forall_ h1_1_v h1_1_phi))
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ ¬isFreeIn h1_1_v h1_1_phi