proposition: Lemma aforallbi_spec : forall A (f : int -> A -> bool) t, aforallbi f t = true <-> forall i, i <? length t = true -> f i (t.[i]) = true.
proof: Proof. intros A f t; unfold aforallbi. split. intro H; generalize (afold_left_andb_true_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_andb_true. 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