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


DEBUG:Going to execute:
induction l; simpl
DEBUG LTAC Evaluated term: (IHl l' H)
DEBUG LTAC Evaluated term: IHl