proposition: Lemma empty_mapsto_iff x e : MapsTo x e empty <-> False.
proof: Proof. rewrite <- find_spec, empty_spec. now split. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)