Goal:
  
  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:
congruence