proposition: Lemma Disjoint_sym m1 m2 : Disjoint m1 m2 -> Disjoint m2 m1.
proof: Proof. intros H k (H1,H2). elim (H k); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)