proposition: Lemma eqb_eq x y : eqb x y = true <-> K.eq x y.
proof: Proof. unfold eqb; case K.eq_dec; now intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)