Goal:
  
  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
  b : B
  Heq : f n a = Some b
  Heq' : map_option_out (mapi_rec f l (S n)) = None
  H : None = Some l'
  H0 : 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:
solve
[ do
![ solve
 [ trivial | apply : eq_sym ; trivial ]
 | discriminate
 | contradiction
 | split ]
| case not_locked_false_eq_true; assumption
| match goal with
  | H:~ _ |- _ => solve [ case H; trivial ]
  end ]