proposition: Lemma afold_left_andb_true : forall a, (forall i, i <? length a = true -> a.[i] = true) -> afold_left bool true andb a = true.
proof: Proof. intros a H. rewrite afold_left_spec by apply andb_true_l; apply foldi_ind. apply leb_0. reflexivity. intros b j _ H1 H2; rewrite H2; simpl; rewrite H; trivial. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz