Fixpoint arrayMipMapLayerCountForLevel
  (level : nat)
  (m     : list arrayMipMap)
: nat :=
  match m with
  | []        => 0
  | (x :: xs) =>
    match Nat.eq_dec (arrayMipMapLevel (arrayMipMapIndex x)) level with
    | left _  => 1 + (arrayMipMapLayerCountForLevel level xs)
    | right _ => (arrayMipMapLayerCountForLevel level xs)
    end
  end.
