proposition: Lemma not_empty_in m : ~Empty m -> exists k, In k m.
proof: Proof. intro. destruct (not_empty_mapsto H) as (k,Hk). now exists k. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)