Goal:
    A : Type  n : nat
  ============================
   (∀ l : list A, #|l| ≤ n → skipn n l = [])


DEBUG:Going to execute:
induction n

Goals:
    A : Type
  ============================
   (∀ l : list A, #|l| ≤ 0 → skipn 0 l = [])

    A : Type  n : nat  IHn : ∀ l : list A, #|l| ≤ n → skipn n l = []
  ============================
   (∀ l : list A, #|l| ≤ S n → skipn (S n) l = [])


DEBUG:Going to execute:
intros l h
DEBUG LTAC Evaluated term: n