Goal:
    A : Type  n : nat  k : nat  p : nat → A → bool  l : list A
  ============================
   (alli p (n + k) l = alli (λ i : nat, p (n + i)) k l)


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

Goals:
    A : Type  n : nat  k : nat  p : nat → A → bool
  ============================
   (alli p (n + k) [] = alli (λ i : nat, p (n + i)) k [])

  
  A : Type
  n : nat
  k : nat
  p : nat → A → bool
  a : A
  l : list A
  IHl : ∀ (n k : nat) (p : nat → A → bool),
          alli p (n + k) l = alli (λ i : nat, p (n + i)) k l
  ============================
   (alli p (n + k) (a :: l) = alli (λ i : nat, p (n + i)) k (a :: l))


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

Goals:
    A : Type  n : nat  k : nat  p : nat → A → bool
  ============================
   (true = true)

  
  A : Type
  n : nat
  k : nat
  p : nat → A → bool
  a : A
  l : list A
  IHl : ∀ (n k : nat) (p : nat → A → bool),
          alli p (n + k) l = alli (λ i : nat, p (n + i)) k l
  ============================
   (p (n + k) a && alli p (S (n + k)) l =
    p (n + k) a && alli (λ i : nat, p (n + i)) (S k) l)


DEBUG:Going to execute:
auto

Goals:
    A : Type  n : nat  k : nat  p : nat → A → bool
  ============================
   (true = true)

  
  A : Type
  n : nat
  k : nat
  p : nat → A → bool
  a : A
  l : list A
  IHl : ∀ (n k : nat) (p : nat → A → bool),
          alli p (n + k) l = alli (λ i : nat, p (n + i)) k l
  ============================
   (p (n + k) a && alli p (S (n + k)) l =
    p (n + k) a && alli (λ i : nat, p (n + i)) (S k) l)


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