cases h1_1
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P ∨ h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
case inl
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)

case inr
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)