Goal:
    A : Type  B : Type  f : A → B  l : list A  H : l ≠ []
  ============================
   (map f l ≠ [])


DEBUG:Going to execute:
destruct l

Goals:
    A : Type  B : Type  f : A → B  H : [] ≠ []
  ============================
   (map f [] ≠ [])

    A : Type  B : Type  f : A → B  a : A  l : list A  H : a :: l ≠ []
  ============================
   (map f (a :: l) ≠ [])


DEBUG:Going to execute:
intro e
DEBUG LTAC Evaluated term: l