apply IsProofAlt.gen_
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt (forall_ h1_1_v h1_1_phi)
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt h1_1_phi