Theorem finset.insert_singelton_self_eq

feat(data/analysis): calculations with filters / topologies + misc

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

feat(data/finset): add fold; add simp rules for insert, empty, singleton and mem