Record typeName := TNMake {
  (** The name of the type. *)
  tnName  : string;
  (** Type names are valid. *)
  tnValid : validName tnName
}.
