Definition binaryIdentifierSection (i : identifier) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D5F494421);
    ("size", u64 (binarySizePadded16 (binaryIdentifier i)));
    ("data", binaryIdentifier i)
  ].
