In some cases we want to express locally that the objects of a given type have unique identifiers.
The attached file contains code that illustrates how this works for structures and a failing/not admissible example with a group within a structure.
The question is, how to get such an invariant admissible for groups.