Goal:
    A : Type  B : Type  P : B → Type  f : nat → A → B  l : list A  k : nat
  ============================
   (Alli (λ (i : nat) (x : A), P (f i x)) k l → All P (mapi_rec f l k))


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  B : Type  P : B → Type  f : nat → A → B  n : nat
  ============================
   (All P (mapi_rec f [] n))

  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (All P (mapi_rec f (hd :: tl) n))


DEBUG:Going to execute:
simpl

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

  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (All P (f n hd :: mapi_rec f tl (S n)))


DEBUG:Going to execute:
constructor

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

  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (All P (f n hd :: mapi_rec f tl (S n)))


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

Goals:
  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (P (f n hd))

  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (All P (mapi_rec f tl (S n)))


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (P (f n hd))

  
  A : Type
  B : Type
  P : B → Type
  f : nat → A → B
  n : nat
  hd : A
  tl : list A
  p : P (f n hd)
  X : Alli (λ (i : nat) (x : A), P (f i x)) (S n) tl
  IHX : All P (mapi_rec f tl (S n))
  ============================
   (All P (mapi_rec f tl (S n)))


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