Goal:
  
  A : Type
  n : nat
  s : list A
  x : A
  xs : list A
  IHn : ∀ (s : list A) (x : A) (xs : list A),
          skipn n s = x :: xs → skipn (S n) s = xs
  ============================
   (skipn (S n) s = x :: xs → skipn (S (S n)) s = xs)


DEBUG:Going to execute:
destruct s

Goals:
  
  A : Type
  n : nat
  x : A
  xs : list A
  IHn : ∀ (s : list A) (x : A) (xs : list A),
          skipn n s = x :: xs → skipn (S n) s = xs
  ============================
   (skipn (S n) [] = x :: xs → skipn (S (S n)) [] = xs)

  
  A : Type
  n : nat
  a : A
  s : list A
  x : A
  xs : list A
  IHn : ∀ (s : list A) (x : A) (xs : list A),
          skipn n s = x :: xs → skipn (S n) s = xs
  ============================
   (skipn (S n) (a :: s) = x :: xs → skipn (S (S n)) (a :: s) = xs)


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