Goal:
  
  A : Type
  a : A
  l : list A
  i : nat
  IHl : ∀ i : nat,
          match nth_error l i with
          | Some a => skipn i l = a :: skipn (S i) l
          | None => skipn i l = []
          end
  ============================
   match nth_error l i with
   | Some a => skipn i l = a :: skipn (S i) l
   | None => skipn i l = []
   end


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