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

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