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:
set (aux := faux)