Goal:
    A : Type  l : list A  l' : list A  n : nat  t : A
  ============================
   (nth_error l n = Some t → nth_error (l ++ l') n = Some t)


DEBUG:Going to execute:
induction l in n |- *; destruct n; simpl