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