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


DEBUG:Going to execute:
destruct l'
DEBUG LTAC Evaluated term: l

Goals:
  
  A : Type
  a : A
  d : A
  IHl : ∀ l' : list A, l' ≠ [] → last ([] ++ l') d = last l' d
  H : [] ≠ []
  ============================
   (a = last [] d)

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


DEBUG:Going to execute:
congruence
DEBUG LTAC Evaluated term: l'

Goals:
  
  A : Type
  a : A
  d : A
  IHl : ∀ l' : list A, l' ≠ [] → last ([] ++ l') d = last l' d
  H : [] ≠ []
  ============================
   (a = last [] d)

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


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