Goal:
    A : Type  n : nat
  ============================
   (∀ n : nat, nth_error [] (S n) = None)


DEBUG:Going to execute:
trivial; hnf; intros