(** For the sake of specification simplicity, we assume that all
    strings are valid regular expressions. *)
Parameter regex : forall (s : string), RegularExpressionT s.
