proposition: Lemma not_empty_mapsto m : ~Empty m -> exists k e, MapsTo k e m.
proof: Proof. intro. destruct (@cardinal_inv_2b m) as ((k,e),H'). contradict H. now apply cardinal_inv_1. exists k; now exists e. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)