proposition: Lemma binds_impl_dom_impl : forall A `{Inhab B} (M:map A B) x v, binds_impl M x v -> x \in dom_impl M.
proof: Proof. Proof using. introv IB K. unfolds binds_impl, dom_impl. rew_set. congruence. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)