Goal:
  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  P : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  Ha : Alli P (S n) tl
  Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
  IHHa : ∀ t : list B,
           map_option_out (mapi_rec f tl (S n)) = Some t
           → map_option_out (mapi_rec g tl (S n)) = Some t
  ============================
   (∀ t : list B,
      map_option_out (mapi_rec f (hd :: tl) n) = Some t
      → map_option_out (mapi_rec g (hd :: tl) n) = Some t)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  P : nat → A → Type
  n : nat
  Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
  ============================
   (∀ t : list B,
      map_option_out (mapi_rec f [] n) = Some t
      → map_option_out (mapi_rec g [] n) = Some t)

  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  P : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  Ha : Alli P (S n) tl
  Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
  IHHa : ∀ t : list B,
           map_option_out (mapi_rec f tl (S n)) = Some t
           → map_option_out (mapi_rec g tl (S n)) = Some t
  ============================
   (∀ t : list B,
      map_option_out (mapi_rec f (hd :: tl) n) = Some t
      → map_option_out (mapi_rec g (hd :: tl) n) = Some t)


DEBUG:Going to execute:
auto
Level 0: Backtrace:

In environment
A : Type
B : Type
f, g : nat → A → option B
P : nat → A → Type
n : nat
hd : A
tl : list A
p : P n hd
Ha : Alli P (S n) tl
Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
IHHa : ∀ t : list B,
         map_option_out (mapi_rec f tl (S n)) = Some t
         → map_option_out (mapi_rec g tl (S n)) = Some t
t : list B
H : map_option_out (mapi_rec f (hd :: tl) n) = Some t
Unable to unify "Some t" with "map_option_out (mapi_rec g (hd :: tl) n)".
Level 0: Backtrace:

In environment
A : Type
B : Type
f, g : nat → A → option B
P : nat → A → Type
n : nat
hd : A
tl : list A
p : P n hd
Ha : Alli P (S n) tl
Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
IHHa : ∀ t : list B,
         map_option_out (mapi_rec f tl (S n)) = Some t
         → map_option_out (mapi_rec g tl (S n)) = Some t
t : list B
H : map_option_out (mapi_rec f (hd :: tl) n) = Some t
Unable to unify "Some t" with "map_option_out (mapi_rec g (hd :: tl) n)".

Goals:
  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  P : nat → A → Type
  n : nat
  Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
  ============================
   (∀ t : list B,
      map_option_out (mapi_rec f [] n) = Some t
      → map_option_out (mapi_rec g [] n) = Some t)

  
  A : Type
  B : Type
  f : nat → A → option B
  g : nat → A → option B
  P : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  Ha : Alli P (S n) tl
  Hfg : ∀ (i : nat) (x : A) (t : B), P i x → f i x = Some t → g i x = Some t
  IHHa : ∀ t : list B,
           map_option_out (mapi_rec f tl (S n)) = Some t
           → map_option_out (mapi_rec g tl (S n)) = Some t
  ============================
   (∀ t : list B,
      map_option_out (mapi_rec f (hd :: tl) n) = Some t
      → map_option_out (mapi_rec g (hd :: tl) n) = Some t)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3