Goal:
    A : Type
  ============================
   match nth_error [] 0 with
   | Some a => skipn 0 [] = a :: skipn 1 []
   | None => skipn 0 [] = []
   end


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: i