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


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3
DEBUG LTAC Evaluated term: (IHl [a])
DEBUG LTAC Evaluated term: (IHl [a])
DEBUG LTAC Evaluated term: IHl
DEBUG LTAC Evaluated term: IHl
DEBUG LTAC Evaluated term: (a :: acc)
DEBUG LTAC Evaluated term: ([a] ++ acc)