Goal:
  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : A -> C -> A
  h : C -> B
  l' : list C
  acc : A
  hfg : forall (acc : A) (x : C), f acc (h x) = g acc x
  ============================
   (fold_left f (map h l') acc = fold_left g l' acc)


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

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

  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : A -> C -> A
  h : C -> B
  a : C
  l' : list C
  acc : A
  hfg : forall (acc : A) (x : C), f acc (h x) = g acc x
  IHl' : forall acc : A, fold_left f (map h l') acc = fold_left g l' acc
  ============================
   (fold_left f (map h (a :: l')) acc = fold_left g (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 : A -> C -> A
  h : C -> B
  acc : A
  hfg : forall (acc : A) (x : C), f acc (h x) = g acc x
  ============================
   (acc = acc)

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


DEBUG:Going to execute:
auto

Goals:
  
  G : t
  A : Type
  B : Type
  C : Type
  f : A -> B -> A
  g : A -> C -> A
  h : C -> B
  acc : A
  hfg : forall (acc : A) (x : C), f acc (h x) = g acc x
  ============================
   (acc = acc)

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


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