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

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