proposition: Lemma xforall_spec A (f:key->A->bool) m i : xforall f m i = List.forallb (fun '(k,e) => f (i@k) e) (bindings m).
proof: Proof. revert i. induction m; simpl; intros; auto. rewrite bindings_node, !forallb_app, IHm1, IHm2. destruct o; simpl. - unfold rev. destruct f; simpl. + rewrite <- andb_lazy_alt. f_equal; rewrite forallb_map; f_equiv; now intros (k,e) ? <-. + now rewrite andb_false_r. - rewrite <- andb_lazy_alt. f_equal; rewrite forallb_map; f_equiv; now intros (k,e) ? <-. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)