proposition: Lemma keyb_eq_equivalence elt : Equivalence (@keyb_eq elt).
proof: Proof. unfold keyb_eq. split; intros; hnf; intros. split; auto. reflexivity. destruct H; split; auto. symmetry; auto. destruct H, H0; split; try congruence. rewrite H; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)