fact: Definition option_filter A (f:key->A->bool) k (o:option A) := match o with | Some a => if f k a then o else None | None => o end.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)