fact: Definition keyb_eq [elt] (x y : key * elt) := K.eq (fst x) (fst y) /\ snd x = snd y.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)