Lemma indexArrayWFElementsNonEmptyDecidable : forall i,
  {indexArrayWFElementsNonEmpty i}+{~indexArrayWFElementsNonEmpty i}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
