Lemma arrayMipMapsNonEmpty : forall (m : arrayMipMapList),
  [] <> arrayMipMaps m.
Proof.
  (* Proof omitted for brevity; see ArrayMipMap.v for proofs. *)
Qed.
