Theorem roleNameDec : forall (a b : roleName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Roles.v for proofs. *)
Qed.
