Goal:
    A : Type  n : nat  l : list A
  ============================
   (#|skipn n l| = #|l| - n)


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

Goals:
    A : Type  n : nat
  ============================
   (#|skipn n []| = #|[]| - n)

  
  A : Type
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (#|skipn n (a :: l)| = #|a :: l| - n)


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

Goals:
    A : Type
  ============================
   (#|skipn 0 []| = #|[]| - 0)

    A : Type  n : nat
  ============================
   (#|skipn (S n) []| = #|[]| - S n)

    A : Type  a : A  l : list A  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (#|skipn 0 (a :: l)| = #|a :: l| - 0)

  
  A : Type
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (#|skipn (S n) (a :: l)| = #|a :: l| - S n)


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

Goals:
    A : Type
  ============================
   (0 = 0)

    A : Type  n : nat
  ============================
   (0 = 0)

    A : Type  a : A  l : list A  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (S #|l| = S #|l|)

  
  A : Type
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (#|skipn n l| = #|l| - n)


DEBUG:Going to execute:
auto

Goals:
    A : Type
  ============================
   (0 = 0)

    A : Type  n : nat
  ============================
   (0 = 0)

    A : Type  a : A  l : list A  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (S #|l| = S #|l|)

  
  A : Type
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, #|skipn n l| = #|l| - n
  ============================
   (#|skipn n l| = #|l| - n)


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