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