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