Goal:
    A : Type  B : Type  f : A → B  l : list A  p : B → bool
  ============================
   (forallb p (map f l) = forallb (λ x : A, p (f x)) l)


DEBUG:Going to execute:
induction l in p, f |- *; simpl; rewrite ?andb_and