Goal:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  l : list A
  l' : list B
  i : nat
  t : B
  ============================
   (map_option_out (mapi_rec f l 0) = Some l' ->
    nth_error l' i = Some t ->
    ∑ x : A, nth_error l i = Some x /\ f i x = Some t)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2