proposition: Lemma singleton_o2 x y e : ~K.eq x y -> find y (singleton x e) = None.
proof: Proof. intros H. rewrite <- not_in_find. contradict H. destruct H as (e' & H). now rewrite singleton_mapsto_iff in H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)