proposition: Lemma disjoint_eq_not_indom_both : forall A B (M1 M2:map A B), disjoint M1 M2 = (forall k, k \indom M1 -> k \indom M2 -> False).
proof: Proof. Proof using. extens. unfold disjoint_impl. rewrite* set_disjoint_eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)