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