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


DEBUG:Going to execute:
induction l in n, k |- *

Goals:
    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   (mapi_rec f [] (n + k) = mapi_rec (λ (k : nat) (x : A), f (n + k) x) [] k)

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


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   ([] = [])

  
  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:
auto

Goals:
    A : Type  B : Type  f : nat → A → B  n : nat  k : nat
  ============================
   ([] = [])

  
  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:
<coq-core.plugins.ltac::auto@0> $1 $2 $3