induction h1
F : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ F
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
⊢ IsDeduct Δ (forall_ v F)
case axiom_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (forall_ v phi✝)

case assume_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct Δ (forall_ v phi✝)

case mp_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct Δ (forall_ v (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (forall_ v phi✝)
⊢ IsDeduct Δ (forall_ v psi✝)