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