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


DEBUG:Going to execute:
destruct l
Level 0: Backtrace:

Tactic failure: congruence failed.
Level 0: Backtrace:

Tactic failure: congruence failed.

Goals:
  
  A : Type
  a : A
  d : A
  d' : A
  IHl : [] ≠ [] → last [] d = last [] d'
  H : [a] ≠ []
  ============================
   (a = a)

  
  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 ≠ []
  ============================
   (last (a0 :: l) d = last (a0 :: l) d')


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: l

Goals:
  
  A : Type
  a : A
  d : A
  d' : A
  IHl : [] ≠ [] → last [] d = last [] d'
  H : [a] ≠ []
  ============================
   (a = a)

  
  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 ≠ []
  ============================
   (last (a0 :: l) d = last (a0 :: l) d')


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