Record attributeName := ANMake { (** The name of the attribute. *) anName : name; (** Attribute names are valid. *) anValid : nameValid anName }.
Record attributeValue := AVMake { (** The value of the attribute. *) avValue : name; (** Attribute values are valid. *) avValid : nameValid avValue }.
Theorem attributeNameDec : forall (a b : attributeName), {a = b}+{a <> b}. Proof. (* Proof omitted for brevity; see Attributes.v for proofs. *) Qed.
Theorem attributeValueDec : forall (a b : attributeValue), {a = b}+{a <> b}. Proof. (* Proof omitted for brevity; see Attributes.v for proofs. *) Qed.