proposition: Lemma indom_union_eq : forall A B (IB:Inhab B) (M1 M2:map A B) x, x \indom (union M1 M2) = (x \indom M1 \/ x \indom M2).
proof: Proof. Proof using. intros. rewrite dom_union. rewrite in_union_eq. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)