`image_set_system` (now `classical_sets.v`) could be used to simplify `subspace_topology.v` fyi: @mkerjean
image_set_system(nowclassical_sets.v) could be used to simplifysubspace_topology.vfyi: @mkerjean