Goal:
    A : Type  s : list A  x : A  xs : list A
  ============================
   (s = x :: xs → match s with
                  | [] => []
                  | _ :: l => l
                  end = xs)


DEBUG:Going to execute:
intros ->
DEBUG LTAC Evaluated term: skipn_0
DEBUG LTAC Evaluated term: n