renamings and new material
generalized local_typedef_ab_group_add
relaxed assumptions for dim_image_eq and dim_image_le
example for Types_To_Sets: transfer from type-based linear algebra to subspaces