HOL-Types_To_Sets.Group_On_With