fact: Fixpoint xforall A (f:key->A->bool) m j := match m with | Leaf => true | Node l None r => xforall f l (j~0) &&& xforall f r (j~1) | Node l (Some e) r => f (rev j) e &&& xforall f l (j~0) &&& xforall f r (j~1) end.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)