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:
<coq-core.plugins.ltac::discriminate@0>