induction h1
F : Formula
Δ Γ : Set Formula
h1 : IsDeduct Γ F
h2 : ∀ H ∈ Γ, IsDeduct Δ H
⊢ IsDeduct Δ F
case axiom_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ phi✝

case assume_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : phi✝ ∈ Γ
⊢ IsDeduct Δ phi✝

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