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