(** A proposition that states that a given regular expression
    matches a given string. *)
Parameter matches : forall (s : string) {e : string},
  RegularExpressionT e -> Prop.
