proposition: Lemma aexistsbi_false_spec : forall A (f : int -> A -> bool) t, aexistsbi f t = false <-> forall i, i <? length t = true -> f i (t.[i]) = false.
proof: Proof. intros A f t; unfold aexistsbi. split. intro H; generalize (afold_left_orb_false_inv _ H); clear H. rewrite length_amapi; intros H i Hi. rewrite <- get_amapi by exact Hi. apply H; exact Hi. intro H; apply afold_left_orb_false. intro i; rewrite length_amapi; intro Hi; rewrite get_amapi by exact Hi; apply H; exact Hi. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz