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


DEBUG:Going to execute:
induction l

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

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


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

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

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


DEBUG:Going to execute:
congruence

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

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


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