Theorem structureValueHasStructureTypeDecidable : forall sv st,
  {structureValueHasStructureType sv st}+{~structureValueHasStructureType sv st}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
