exact h1_ih_1
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
no goals