Goal:
    A : Type  B : Type  f : B  l : list A
  ============================
   ((fix map (l : list A) : list B :=
       match l with
       | [] => []
       | _ :: t => f :: map t
       end) l = repeat f #|l|)


DEBUG:Going to execute:
induction l

Goals:
    A : Type  B : Type  f : B
  ============================
   ([] = repeat f #|[]|)

  
  A : Type
  B : Type
  f : B
  a : A
  l : list A
  IHl : (fix map (l : list A) : list B :=
           match l with
           | [] => []
           | _ :: t => f :: map t
           end) l = repeat f #|l|
  ============================
   (f
    :: (fix map (l : list A) : list B :=
          match l with
          | [] => []
          | _ :: t => f :: map t
          end) l = repeat f #|a :: l|)


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

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

  
  A : Type
  B : Type
  f : B
  a : A
  l : list A
  IHl : (fix map (l : list A) : list B :=
           match l with
           | [] => []
           | _ :: t => f :: map t
           end) l = repeat f #|l|
  ============================
   (f
    :: (fix map (l : list A) : list B :=
          match l with
          | [] => []
          | _ :: t => f :: map t
          end) l = f :: repeat f #|l|)


DEBUG:Going to execute:
auto

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

  
  A : Type
  B : Type
  f : B
  a : A
  l : list A
  IHl : (fix map (l : list A) : list B :=
           match l with
           | [] => []
           | _ :: t => f :: map t
           end) l = repeat f #|l|
  ============================
   (f
    :: (fix map (l : list A) : list B :=
          match l with
          | [] => []
          | _ :: t => f :: map t
          end) l = f :: repeat f #|l|)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3