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 => _).