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

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