Inductive ShortNameT :=
  ShortName : forall (s : string),
    matches s (regex "[a-z][a-z0-9_-]{0,128}")
      -> ShortNameT.
