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


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