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


DEBUG:Going to execute:
induction l

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

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


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

Goals:
    A : Type  d : A  d' : A
  ============================
   ([] ≠ [] → d = d')

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


DEBUG:Going to execute:
try congruence