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


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1
DEBUG LTAC Evaluated term: IHl