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