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