proposition: Lemma afold_left_and A (p : A -> bool) a : afold_left bool true andb (amap p a) = List.forallb p (to_list a).
proof: Proof. rewrite afold_left_spec, foldi_to_list, to_list_amap by exact andb_true_l. rewrite <- andb_true_r. generalize true. induction (to_list a) as [ | x l ]; clear a; intro b. reflexivity. simpl; rewrite IHl. rewrite (andb_comm b (p x)), (andb_comm (p x) (forallb p l)); apply andb_assoc. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz