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


DEBUG:Going to execute:
set (aux := faux)