proposition: Lemma read_of_binds : forall A `{Inhab B} (M:map A B) x v, binds M x v -> M[x] = v.
proof: Proof. Proof using. introv K. rewrite* (@binds_eq_indom_read A B H) in K. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)