Record actionName := ANMake { (** The name of the action. *) anName : string; (** Action names are valid. *) anValid : validName anName }.
Theorem actionNameDec : forall (a b : actionName), {a = b}+{a <> b}. Proof. (* Proof omitted for brevity; see Actions.v for proofs. *) Qed.
Record action : Set := AMake { aName : actionName }.