proposition: Lemma aforallbi_false_spec : forall A (f : int -> A -> bool) t, aforallbi f t = false <-> exists i, i <? length t = true /\ f i (t.[i]) = false.
proof: Proof. intros A f t; unfold aforallbi. split. intro H; generalize (afold_left_andb_false_inv _ H); clear H. intros [ i [ Hi Hf ] ]; exists i. rewrite length_amapi in Hi; rewrite get_amapi in Hf by exact Hi. split; [ exact Hi | exact Hf ]. intros [ i [ Hi Hf ] ]. apply (afold_left_andb_false i); [ rewrite length_amapi; exact Hi | rewrite get_amapi by exact Hi; exact Hf ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz