Inductive FileNameT :=
  FileName : forall (s : string),
    matches s (regex "([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*")
      -> FileNameT.
