Lemma indexArrayWFElementsLtDataSizeDecidable : forall dataSize i,
  {indexArrayWFElementsLtDataSize dataSize i}+{~indexArrayWFElementsLtDataSize dataSize i}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
