Theorem finset.erase_dup_map_erase_dup_eq

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