fact: Parameter binds_eq_indom_read : forall A `{Inhab B} (M:map A B) x v, (binds M x v) = (x \indom M /\ M[x] = v).
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet LibContainer LibMap)