Goal:
  
  A : Type
  B : Type
  f : nat → A → B
  a : A
  l : list A
  n : nat
  k : nat
  IHl : ∀ n k : nat,
          mapi_rec f l (n + k) =
          mapi_rec (λ (k0 : nat) (x : A), f (n + k0) x) l k
  ============================
   (f (n + k) a :: mapi_rec f l (S (n + k)) =
    f (n + k) a :: mapi_rec (λ (k : nat) (x : A), f (n + k) x) l (S k))


DEBUG:Going to execute:
f_equal