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


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