apply IsAxiom.pred_3_
case a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsAxiom (h1_phi.imp_ (forall_ h1_v h1_phi))
case a.a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ ¬isFreeIn h1_v h1_phi