Goal:
  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  a : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k (mapi_rec f l k)
          → Alli (λ (n : nat) (a : A), P n (f n a)) k l
  X : Alli P k (f k a :: mapi_rec f l (S k))
  hd : B
  tl : list B
  X0 : P k (f k a)
  X1 : Alli P (S k) (mapi_rec f l (S k))
  H0 : hd = f k a
  H1 : tl = mapi_rec f l (S k)
  ============================
   (Alli (λ (n : nat) (a : A), P n (f n a)) k (a :: l))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  a : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k (mapi_rec f l k)
          → Alli (λ (n : nat) (a : A), P n (f n a)) k l
  X : Alli P k (f k a :: mapi_rec f l (S k))
  hd : B
  tl : list B
  X0 : P k (f k a)
  X1 : Alli P (S k) (mapi_rec f l (S k))
  H0 : hd = f k a
  H1 : tl = mapi_rec f l (S k)
  ============================
   (P k (f k a))

  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  a : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k (mapi_rec f l k)
          → Alli (λ (n : nat) (a : A), P n (f n a)) k l
  X : Alli P k (f k a :: mapi_rec f l (S k))
  hd : B
  tl : list B
  X0 : P k (f k a)
  X1 : Alli P (S k) (mapi_rec f l (S k))
  H0 : hd = f k a
  H1 : tl = mapi_rec f l (S k)
  ============================
   (Alli (λ (n : nat) (a : A), P n (f n a)) (S k) l)


DEBUG:Going to execute:
eauto

Goals:
  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  a : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k (mapi_rec f l k)
          → Alli (λ (n : nat) (a : A), P n (f n a)) k l
  X : Alli P k (f k a :: mapi_rec f l (S k))
  hd : B
  tl : list B
  X0 : P k (f k a)
  X1 : Alli P (S k) (mapi_rec f l (S k))
  H0 : hd = f k a
  H1 : tl = mapi_rec f l (S k)
  ============================
   (P k (f k a))

  
  A : Type
  B : Type
  P : nat → B → Type
  f : nat → A → B
  k : nat
  a : A
  l : list A
  IHl : ∀ k : nat,
          Alli P k (mapi_rec f l k)
          → Alli (λ (n : nat) (a : A), P n (f n a)) k l
  X : Alli P k (f k a :: mapi_rec f l (S k))
  hd : B
  tl : list B
  X0 : P k (f k a)
  X1 : Alli P (S k) (mapi_rec f l (S k))
  H0 : hd = f k a
  H1 : tl = mapi_rec f l (S k)
  ============================
   (Alli (λ (n : nat) (a : A), P n (f n a)) (S k) l)


DEBUG:Going to execute:
<coq-core.plugins.ltac::eauto@0> $1 $2 $3