Goal:
    A : Type  B : Type  f : A → B
  ============================
   (∀ l : list 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 []| = #|l|)


DEBUG:Going to execute:
match goal with
           | |- context [ #|?faux _ _| ] => set (aux := faux)
           end
DEBUG LTAC Evaluated term: h