proposition: Lemma singleton_mapsto_iff x y e e' : MapsTo y e' (singleton x e) <-> K.eq x y /\ e = e'.
proof: Proof. rewrite <- bindings_spec1, singleton_spec, InA_cons, InA_nil. unfold Duo; simpl; intuition (auto with map). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)