Goal:
  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  l : list A
  t : list B
  P : nat → A → Type
  ============================
   (∀ n : nat,
      Alli P n l
      → (∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t)
        → map_option_out (mapi_rec f l n) = Some t
          → map_option_out (mapi_rec g l n) = Some t)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2
DEBUG LTAC Evaluated term: 0