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