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


DEBUG:Going to execute:
match goal with
           | |- ∀ l a, ?faux _ _ = _ => set (aux := faux)
           end
DEBUG LTAC Evaluated term: h