Definition binaryClipsDataSection (c : clips) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D434C4950);
    ("size", u64 (binarySizePadded16 (binaryClipsDataSectionAudio c)));
    ("data", binaryClipsDataSectionAudio c)
  ].
