Goal:
    A : Type  B : Type  f : nat -> A -> option B  i : nat  t : B  n : nat
  ============================
   (None = Some t ->
    ∑ x : A, nth_error [] i = Some x /\ f (i + n)%nat x = Some t)


DEBUG:Going to execute:
discriminate
DEBUG LTAC Evaluated term: nth_error_nil
DEBUG LTAC Evaluated term: nth_error_nil