Goal:
    A : Type  l : list A  x : A
  ============================
   (l ++ [x] ≠ [])


DEBUG:Going to execute:
destruct l

Goals:
    A : Type  x : A
  ============================
   ([] ++ [x] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   ((a :: l) ++ [x] ≠ [])


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

Goals:
    A : Type  x : A
  ============================
   ([x] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   (a :: l ++ [x] ≠ [])


DEBUG:Going to execute:
congruence

Goals:
    A : Type  x : A
  ============================
   ([x] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   (a :: l ++ [x] ≠ [])


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