Goal:
    A : Type  l : list A  d : A
  ============================
   (∀ l' : list A, l' ≠ [] → last (l ++ l') d = last l' d)


DEBUG:Going to execute:
induction l; simpl