Definition indexArrayWFElementsNonEmpty (i : indexArrayT) : Prop :=
  (indexElements i) <> nil.
