Theorem finset.image_to_finset_of_nodup

refactor(data/finset): redefine finsets as subtype of multisets

fix(data/finset): use the type class projections for insert; hide most constants using protected; add image of finset