Record roleName := RNMake {
  (** The name of the role. *)
  rnName  : string;
  (** Role names are valid. *)
  rnValid : validName rnName
}.
