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

case a.a.a
P Q : Formula
⊢ IsDeduct ∅ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))