Goal:
    A : Type  n : nat
  ============================
   (nth_error [] 0 = None)


DEBUG:Going to execute:
trivial; hnf; intros