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

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