Goal:
  
  A : Type
  p : nat → A → bool
  q : nat → A → bool
  l : list A
  l' : list A
  B : Type
  f : B → A
  n : nat
  bs : list B
  ============================
   (alli p n (map f bs) = alli (λ i : nat, p i ∘ f) n bs)


DEBUG:Going to execute:
induction bs in n |- *; simpl