Goal:
  
  A : Type
  B : Type
  C : Type
  g : nat → A → B
  f : nat → B → C
  l : list A
  ============================
   (∀ n : nat,
      mapi_rec f (mapi_rec g l n) n =
      mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l n)


DEBUG:Going to execute:
induction l

Goals:
    A : Type  B : Type  C : Type  g : nat → A → B  f : nat → B → C
  ============================
   (∀ n : nat,
      mapi_rec f (mapi_rec g [] n) n =
      mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) [] n)

  
  A : Type
  B : Type
  C : Type
  g : nat → A → B
  f : nat → B → C
  a : A
  l : list A
  IHl : ∀ n : nat,
          mapi_rec f (mapi_rec g l n) n =
          mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l n
  ============================
   (∀ n : nat,
      mapi_rec f (mapi_rec g (a :: l) n) n =
      mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) (a :: l) n)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  B : Type  C : Type  g : nat → A → B  f : nat → B → C
  ============================
   (nat → [] = [])

  
  A : Type
  B : Type
  C : Type
  g : nat → A → B
  f : nat → B → C
  a : A
  l : list A
  IHl : ∀ n : nat,
          mapi_rec f (mapi_rec g l n) n =
          mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l n
  ============================
   (∀ n : nat,
      f n (g n a) :: mapi_rec f (mapi_rec g l (S n)) (S n) =
      f n (g n a) :: mapi_rec (λ (n0 : nat) (x : A), f n0 (g n0 x)) l (S n))


DEBUG:Going to execute:
try congruence