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; simpl
DEBUG LTAC Evaluated term: 0