apply deduction_theorem
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.not_.imp_ P)
case a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U.not_}) P