proposition: Lemma add_b m x y e : mem y (add x e m) = eqb x y || mem y m.
proof: Proof. rewrite !mem_find_b, add_o. unfold eqb. now destruct (K.eq_dec x y). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)