Goal:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a /\ f n a = Some t)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
do_ccl

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
try do_atom; repeat (do_intro; try do_atom); try arith_congr;
            (solve [ Init.split; do_ccl ])

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
try do_atom; repeat (do_intro; try do_atom); try arith_congr;
            (solve [ Init.split; do_ccl ])

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
try do_atom; repeat (do_intro; try do_atom); try arith_congr

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
try do_atom; repeat (do_intro; try do_atom)

Goals:
  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (Some a = Some a)

  
  A : Type
  B : Type
  f : nat -> A -> option B
  a : A
  l : list A
  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
  Heq : f n a = Some t
  l0 : list B
  Heq' : map_option_out (mapi_rec f l (S n)) = Some l0
  ============================
   (f n a = Some t)


DEBUG:Going to execute:
try do_atom