(** Whether a string matches a regular expression is decidable. *)
Parameter matchesDecidable : forall 
  (s : string)
  {e : string}
  (r : RegularExpressionT e),
    {matches s r}+{~matches s r}.
