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