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