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