Goal:
  
  A : Type
  a : A
  a0 : A
  l : list A
  d : A
  IHl : ∀ l' : list A, l' ≠ [] → last ((a0 :: l) ++ l') d = last l' d
  l' : list A
  H : l' ≠ []
  ============================
   (match l ++ l' with
    | [] => a0
    | _ :: _ => last (l ++ l') d
    end = last l' d)


DEBUG:Going to execute:
<coq-core.plugins.ltac::specialize@0> $1