fact: Definition rew_hd_error : tactic := match_goal with | [[? A (l: list A) |- context C[hd_error l] ]] => match l with | [] => rewrite hd_error_nil | (_ :: _) => rewrite hd_error_cons end end.
imports: Mtac2(Mtac2) Lists.List