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| = #|acc| + #|l|)


DEBUG:Going to execute:
<coq-core.plugins.ltac::intro@1> $1
DEBUG LTAC Evaluated term: (fix aux (l : list A) (acc : list B) {struct l} :
                                list B :=
                              match l with
                              | [] => acc
                              | x :: l0 => aux l0 (f x :: acc)
                              end)
DEBUG LTAC Evaluated term: (∀ (l : list A) (acc : list B),
                              #|aux l acc| = #|acc| + #|l|)