proposition: Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo.
proof: Proof. intros k k' Hk e e' He m m' Hm. red in Hk. now subst. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)