proposition: Lemma Disjoint_alt : forall m m', Disjoint m m' <-> (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False).
proof: Proof. unfold Disjoint; split. intros H k v v' H1 H2. apply H with k; split. exists v; trivial. exists v'; trivial. intros H k ((v,Hv),(v',Hv')). eapply H; eauto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)