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


DEBUG:Going to execute:
rewrite nth_error_nil