proposition: Lemma afold_left_or A (p : A -> bool) a : afold_left bool false orb (amap p a) = List.existsb p (to_list a).
proof: Proof. rewrite afold_left_spec, foldi_to_list, to_list_amap by exact andb_true_l. rewrite <- orb_false_r. generalize false. induction (to_list a) as [ | x l ]; clear a; intro b. reflexivity. simpl; rewrite IHl. rewrite (orb_comm b (p x)), (orb_comm (p x) (existsb p l)); apply orb_assoc. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz