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