proposition: Lemma disjoint_of_not_indom_both : forall A B (M1 M2:map A B), (forall k, k \indom M1 -> k \indom M2 -> False) -> disjoint M1 M2.
proof: Proof. Proof using. introv M. rewrite~ disjoint_eq_not_indom_both. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)