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


DEBUG:Going to execute:
induction l in i, l' |- *

Goals:
    A : Type  B : Type  f : nat -> A -> option B  l' : list B  i : nat  t : B
  ============================
   (forall n : nat,
    map_option_out (mapi_rec f [] n) = Some l' ->
    nth_error l' i = Some t ->
    ∑ x : A, nth_error [] i = Some x /\ f (i + n)%nat x = Some t)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  l' : list B
  i : nat
  t : B
  IHl : forall (l' : list B) (i n : nat),
        map_option_out (mapi_rec f l n) = Some l' ->
        nth_error l' i = Some t ->
        ∑ x : A, nth_error l i = Some x /\ f (i + n)%nat x = Some t
  ============================
   (forall n : nat,
    map_option_out (mapi_rec f (a :: l) n) = Some l' ->
    nth_error l' i = Some t ->
    ∑ x : A, nth_error (a :: l) i = Some x /\ f (i + n)%nat x = Some t)


DEBUG:Going to execute:
intros n
DEBUG LTAC Evaluated term: l

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  l' : list B
  i : nat
  t : B
  n : nat
  ============================
   (map_option_out (mapi_rec f [] n) = Some l' ->
    nth_error l' i = Some t ->
    ∑ x : A, nth_error [] i = Some x /\ f (i + n)%nat x = Some t)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  l' : list B
  i : nat
  t : B
  IHl : forall (l' : list B) (i n : nat),
        map_option_out (mapi_rec f l n) = Some l' ->
        nth_error l' i = Some t ->
        ∑ x : A, nth_error l i = Some x /\ f (i + n)%nat x = Some t
  n : nat
  ============================
   (map_option_out (mapi_rec f (a :: l) n) = Some l' ->
    nth_error l' i = Some t ->
    ∑ x : A, nth_error (a :: l) i = Some x /\ f (i + n)%nat x = Some t)


DEBUG:Going to execute:
simpl