Lemma cubeMipMapsNonEmpty : forall (m : cubeMipMapList),
  [] <> cubeMipMaps m.
Proof.
  (* Proof omitted for brevity; see CubeMipMap.v for proofs. *)
Qed.
