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


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>