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 |- *; simpl