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


DEBUG:Going to execute:
reflexivity