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


DEBUG:Going to execute:
induction l

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

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


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

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

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


DEBUG:Going to execute:
congruence

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

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


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