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

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

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


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

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

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


DEBUG:Going to execute:
auto

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

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


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