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: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface