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


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