Theorem finset.insert_inter_of_not_mem

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

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