Lemma mipMapsNonEmpty : forall (m : mipMapList),
  [] <> mipMaps m.
Proof.
  (* Proof omitted for brevity; see MipMap.v for proofs. *)
Qed.
