proposition: Lemma singleton_o x y e : find y (singleton x e) = if K.eq_dec x y then Some e else None.
proof: Proof. destruct (K.eq_dec x y) as [<-|NE]; auto using singleton_o1, singleton_o2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)