Record typeName := TNMake { (** The name of the type. *) tnName : string; (** Type names are valid. *) tnValid : validName tnName }.
Theorem typeNameDec : forall (a b : typeName), {a = b}+{a <> b}. Proof. (* Proof omitted for brevity; see Objects.v for proofs. *) Qed.
Record object := OMake { (** The object type name. *) oType : typeName; (** The attributes held by the object. *) oAttributes : AttributeNameMaps.t attributeValue }.