Record roleName := RNMake { (** The name of the role. *) rnName : string; (** Role names are valid. *) rnValid : validName rnName }.
Theorem roleNameDec : forall (a b : roleName), {a = b}+{a <> b}. Proof. (* Proof omitted for brevity; see Roles.v for proofs. *) Qed.