proposition: Lemma binds_inj : forall A i `{Inhab B} v1 v2 (M:map A B), binds M i v1 -> binds M i v2 -> v1 = v2.
proof: Proof. Proof using. introv IB H1 H2. rewrite (@binds_eq_indom_read A B IB) in *. destruct H1; destruct H2. congruence. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)