Goal:
  
  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
  H : [] = x :: xs
  ============================
   ([] = xs)


DEBUG:Going to execute:
PTRDEBUGTAC<coq-core.plugins.ltac::discriminate@0>