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