proposition: Lemma read_union_cases : forall A B (IB:Inhab B) (M1 M2:map A B) x, read (union M1 M2) x = (If x \indom M2 then M2[x] else M1[x]).
proof: Proof. Proof using. intros. unfold read, read_inst, read_impl. unfold dom, dom_inst, dom_impl. rewrite in_set_st_eq. unfold union, union_inst, union_impl. case_eq (M2 x); introv Hv2; case_if; congruence. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)