Goal:
    A : Type  l : list A  hd : A  tl : list A
  ============================
   (skipn 0 l = hd :: tl → nth_error l 0 = Some hd ∧ skipn 1 l = tl)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrtclintros@0> arg
DEBUG LTAC Evaluated term: n