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
  ============================
   (match f n hd with
    | Some hd =>
        match map_option_out (mapi_rec f tl (S n)) with
        | Some tl => Some (hd :: tl)
        | None => None
        end
    | None => None
    end = Some t
    → match g n hd with
      | Some hd =>
          match map_option_out (mapi_rec g tl (S n)) with
          | Some tl => Some (hd :: tl)
          | None => None
          end
      | None => None
      end = Some t)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrcase@0> $1 $2

Goals:
  
  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
  b : B
  E : f n hd = Some b
  ============================
   (match map_option_out (mapi_rec f tl (S n)) with
    | Some tl => Some (b :: tl)
    | None => None
    end = Some t
    → match g n hd with
      | Some hd =>
          match map_option_out (mapi_rec g tl (S n)) with
          | Some tl => Some (hd :: tl)
          | None => None
          end
      | None => None
      end = 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
  E : f n hd = None
  ============================
   (None = Some t
    → match g n hd with
      | Some hd =>
          match map_option_out (mapi_rec g tl (S n)) with
          | Some tl => Some (hd :: tl)
          | None => None
          end
      | None => None
      end = Some t)


DEBUG:Going to execute:
try congruence
DEBUG LTAC Evaluated term: (f n hd)