apply generalization
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ (forall_ h1_v h1_phi)
case h1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_phi

case h2
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ ∀ H ∈ ∅, ¬isFreeIn h1_v H