Theorem indexArrayWFDecidable : forall dataSize i,
  {indexArrayWF dataSize i}+{~indexArrayWF dataSize i}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
