proposition: Lemma not_indom_of_indom_disjoint : forall A B (M1 M2:map A B) x, x \indom M1 -> disjoint M1 M2 -> ~ x \indom M2.
proof: Proof. Proof using. introv H1 D H2. rewrite* disjoint_eq_not_indom_both in D. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)