.. coq::

   Tactic Notation "impl_elim" hyp(K) "in" hyp(H) "as" simple_intropattern(P) :=
     pose proof (K H) as P.

   Tactic Notation "impl_elim" hyp(H) :=
     refine (H _).

   Tactic Notation "neg_elim" hyp(H) ", " hyp(notH) :=
     exact (notH H).

   Tactic Notation "neg_intro" simple_intropattern(P) :=
     refine (fun P => _).