Inductive TagT : Set := Tag {
  tag_byte0 : byte;
  tag_byte1 : byte;
  tag_byte2 : byte;
  tag_byte3 : byte;
  tag_byte4 : byte;
  tag_byte5 : byte;
  tag_byte6 : byte;
  tag_byte7 : byte
}.
