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


DEBUG:Going to execute:
<coq-core.plugins.ltac::intro@1> $1

Goals:
    A : Type  B : Type  f : A → B  H : [] ≠ []  e : map f [] = []
  ============================
   False

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


DEBUG:Going to execute:
now apply H

Goals:
    A : Type  B : Type  f : A → B  H : [] ≠ []  e : map f [] = []
  ============================
   False

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


DEBUG:Going to execute:
apply H

Goals:
    A : Type  B : Type  f : A → B  H : [] ≠ []  e : map f [] = []
  ============================
   False

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


DEBUG:Going to execute:
t; easy

Goals:
    A : Type  B : Type  f : A → B  H : [] ≠ []  e : map f [] = []
  ============================
   False

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


DEBUG:Going to execute:
t

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

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


DEBUG:Going to execute:
easy
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H

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

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


DEBUG:Going to execute:
easy0 || (solve [ intuition eauto  3 with core terms ])