Goal:
    A : Type  n : nat  acc : list A  l : list A
  ============================
   (split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l))


DEBUG:Going to execute:
induction n in acc, l |- *

Goals:
    A : Type  acc : list A  l : list A
  ============================
   (split_at_aux 0 acc l = (List.rev acc ++ firstn 0 l, skipn 0 l))

  
  A : Type
  n : nat
  acc : list A
  l : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   (split_at_aux (S n) acc l =
    (List.rev acc ++ firstn (S n) l, skipn (S n) l))


DEBUG:Going to execute:
destruct l
DEBUG LTAC Evaluated term: n

Goals:
    A : Type  acc : list A
  ============================
   (split_at_aux 0 acc [] = (List.rev acc ++ firstn 0 [], skipn 0 []))

    A : Type  acc : list A  a : A  l : list A
  ============================
   (split_at_aux 0 acc (a :: l) =
    (List.rev acc ++ firstn 0 (a :: l), skipn 0 (a :: l)))

  
  A : Type
  n : nat
  acc : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   (split_at_aux (S n) acc [] =
    (List.rev acc ++ firstn (S n) [], skipn (S n) []))

  
  A : Type
  n : nat
  acc : list A
  a : A
  l : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   (split_at_aux (S n) acc (a :: l) =
    (List.rev acc ++ firstn (S n) (a :: l), skipn (S n) (a :: l)))


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  acc : list A
  ============================
   ((List.rev acc, []) = (List.rev acc ++ [], []))

    A : Type  acc : list A  a : A  l : list A
  ============================
   ((List.rev acc, a :: l) = (List.rev acc ++ [], a :: l))

  
  A : Type
  n : nat
  acc : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   ((List.rev acc, []) = (List.rev acc ++ [], []))

  
  A : Type
  n : nat
  acc : list A
  a : A
  l : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   (split_at_aux n (a :: acc) l =
    (List.rev acc ++ a :: firstn n l, skipn n l))


DEBUG:Going to execute:
auto

Goals:
    A : Type  acc : list A
  ============================
   ((List.rev acc, []) = (List.rev acc ++ [], []))

    A : Type  acc : list A  a : A  l : list A
  ============================
   ((List.rev acc, a :: l) = (List.rev acc ++ [], a :: l))

  
  A : Type
  n : nat
  acc : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   ((List.rev acc, []) = (List.rev acc ++ [], []))

  
  A : Type
  n : nat
  acc : list A
  a : A
  l : list A
  IHn : ∀ acc l : list A,
          split_at_aux n acc l = (List.rev acc ++ firstn n l, skipn n l)
  ============================
   (split_at_aux n (a :: acc) l =
    (List.rev acc ++ a :: firstn n l, skipn n l))


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3