proposition: Lemma finite_to_finite_fold_support : forall A `{Inhab B} (M:map A B), finite M -> LibSet.finite \set{ p | exists k x, p = (k, x) /\ binds_impl M k x}.
proof: Proof. Proof using. introv IB HM. lets (L&E): finite_inv_list_covers HM. applys finite_of_list_covers (LibList.map (fun x => (x, M[x])) L). intros (k',x') Hk. rew_set. destruct Hk as (k&x&EQ&R). inverts EQ. forwards~: binds_impl_dom_impl R. forwards~ V: E k. lets U: LibList.mem_map (fun x => (x, M[x])) V. applys_eq U. simpl. unfold read_impl. hnf in R. rewrite~ R. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)