Goal:
  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : C -> B
  l : list C
  acc : A
  ============================
   (fold_left f (map g l) acc =
    fold_left (fun (acc : A) (x : C) => f acc (g x)) l acc)


DEBUG:Going to execute:
induction l in acc |- *

Goals:
    G : t  A : Type  B : Type  C : Type  f : A -> B -> A  g : C -> B  acc : A
  ============================
   (fold_left f (map g []) acc =
    fold_left (fun (acc : A) (x : C) => f acc (g x)) [] acc)

  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : C -> B
  a : C
  l : list C
  acc : A
  IHl : forall acc : A,
        fold_left f (map g l) acc =
        fold_left (fun (acc0 : A) (x : C) => f acc0 (g x)) l acc
  ============================
   (fold_left f (map g (a :: l)) acc =
    fold_left (fun (acc : A) (x : C) => f acc (g x)) (a :: l) acc)


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

Goals:
    G : t  A : Type  B : Type  C : Type  f : A -> B -> A  g : C -> B  acc : A
  ============================
   (acc = acc)

  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : C -> B
  a : C
  l : list C
  acc : A
  IHl : forall acc : A,
        fold_left f (map g l) acc =
        fold_left (fun (acc0 : A) (x : C) => f acc0 (g x)) l acc
  ============================
   (fold_left f (map g l) (f acc (g a)) =
    fold_left (fun (acc : A) (x : C) => f acc (g x)) l (f acc (g a)))


DEBUG:Going to execute:
auto

Goals:
    G : t  A : Type  B : Type  C : Type  f : A -> B -> A  g : C -> B  acc : A
  ============================
   (acc = acc)

  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : C -> B
  a : C
  l : list C
  acc : A
  IHl : forall acc : A,
        fold_left f (map g l) acc =
        fold_left (fun (acc0 : A) (x : C) => f acc0 (g x)) l acc
  ============================
   (fold_left f (map g l) (f acc (g a)) =
    fold_left (fun (acc : A) (x : C) => f acc (g x)) l (f acc (g a)))


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