Lemma structureWFComponentNamesUniqueDecidable : forall s,
  {structureWFComponentNamesUnique s}+{~structureWFComponentNamesUnique s}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
