Goal:
  
  A : Type
  B : Type
  f : A → B
  aux := fix aux (l : list A) (acc : list B) {struct l} : list B :=
           match l with
           | [] => acc
           | x :: l0 => aux l0 (f x :: acc)
           end : list A → list B → list B
  l : list A
  ============================
   (∀ acc : list B, aux l acc = aux l [] ++ acc)


DEBUG:Going to execute:
induction l

Goals:
  
  A : Type
  B : Type
  f : A → B
  aux := fix aux (l : list A) (acc : list B) {struct l} : list B :=
           match l with
           | [] => acc
           | x :: l0 => aux l0 (f x :: acc)
           end : list A → list B → list B
  ============================
   (∀ acc : list B, aux [] acc = aux [] [] ++ acc)

  
  A : Type
  B : Type
  f : A → B
  aux := fix aux (l : list A) (acc : list B) {struct l} : list B :=
           match l with
           | [] => acc
           | x :: l0 => aux l0 (f x :: acc)
           end : list A → list B → list B
  a : A
  l : list A
  IHl : ∀ acc : list B, aux l acc = aux l [] ++ acc
  ============================
   (∀ acc : list B, aux (a :: l) acc = aux (a :: l) [] ++ acc)


DEBUG:Going to execute:
intro acc
DEBUG LTAC Evaluated term: l