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
  k0 : nat
  x : A
  H : k ≤ k0
  H0 : k0 < #|l| + k
  ============================
   (S n + k0 = n + S k0)


DEBUG:Going to execute:
idtac