proposition: Lemma union_read_l : forall A `{Inhab B} (m1 m2:map A B) (i:A), i \indom m1 -> dom m1 \# dom m2 -> m1[i] = (m1 \u m2)[i].
proof: Proof. introv M D. rewrite set_disjoint_eq in D. simpl. unfold read_impl, union_impl. cases (m2 i). { false D M. applys~ indom_of_binds. simpl. unfolds* binds_impl. } { cases~ (m1 i). } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)