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
  l : list A
  ============================
   (∀ acc : list A, #|aux l acc| = #|acc| + #|l|)


DEBUG:Going to execute:
induction l

Goals:
  
  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
  ============================
   (∀ acc : list A, #|aux [] acc| = #|acc| + #|[]|)

  
  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| = #|acc| + #|l|
  ============================
   (∀ acc : list A, #|aux (a :: l) acc| = #|acc| + #|a :: l|)


DEBUG:Going to execute:
intro acc
DEBUG LTAC Evaluated term: l