Goal:
    A : Type  m : nat  x : A
  ============================
   (∀ (n : nat) (l : list A),
      nth_error (firstn n l) m = Some x → nth_error l m = Some x)


DEBUG:Going to execute:
induction m; intros n l H; destruct n, l; cbn in *