apply IsDeduct.mp_ P.not_.not_
case h1
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ P)

case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_