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


DEBUG:Going to execute:
induction l

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

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


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

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

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


DEBUG:Going to execute:
congruence

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

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


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