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
  ============================
   (mapi_rec (λ (k : nat) (x : A), f (S n + k) x) l k =
    mapi_rec (λ (k : nat) (x : A), f (n + k) x) l (S k))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2
DEBUG LTAC Evaluated term: (IHl (S n) k)
DEBUG LTAC Evaluated term: (IHl (S n) k)