proposition: Lemma disjoint_eq_disjoint_dom : forall A B (M N:map A B), disjoint M N = disjoint (dom M) (dom N).
proof: Proof. Proof using. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)