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

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