Theorem validNameDecidable : forall s,
  {validName s}+{~validName s}.
Proof.
  (* Proof omitted for brevity; see Names.v for proofs. *)
Qed.
