induction h1
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
Γ : Set Formula
⊢ IsDeduct (Δ ∪ Γ) F
case axiom_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct (Δ ∪ Γ) phi✝

case assume_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) phi✝

case mp_
F : Formula
Δ Γ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct (Δ ∪ Γ) (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct (Δ ∪ Γ) phi✝
⊢ IsDeduct (Δ ∪ Γ) psi✝