Goal:
  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  ============================
   (alli p n (l ++ l') = alli p n l && alli p (#|l| + n) l')


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

Goals:
  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  ============================
   (alli p n ([] ++ l') = alli p n [] && alli p (#|[]| + n) l')

  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  a : A
  l0 : list A
  IHl0 : ∀ n : nat,
           alli p n (l0 ++ l') = alli p n l0 && alli p (#|l0| + n) l'
  ============================
   (alli p n ((a :: l0) ++ l') =
    alli p n (a :: l0) && alli p (#|a :: l0| + n) l')


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

Goals:
  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  ============================
   (alli p n l' = alli p n l')

  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  a : A
  l0 : list A
  IHl0 : ∀ n : nat,
           alli p n (l0 ++ l') = alli p n l0 && alli p (#|l0| + n) l'
  ============================
   (p n a && alli p (S n) (l0 ++ l') =
    p n a && alli p (S n) l0 && alli p (S (#|l0| + n)) l')


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  ============================
   (alli p n l' = alli p n l')

  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  n : nat
  a : A
  l0 : list A
  IHl0 : ∀ n : nat,
           alli p n (l0 ++ l') = alli p n l0 && alli p (#|l0| + n) l'
  ============================
   (p n a && alli p (S n) (l0 ++ l') =
    p n a && alli p (S n) l0 && alli p (S (#|l0| + n)) l')


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