Inductive channelLayoutDescriptionPacked : Set := CLDPMake {
  pChannels         : list channelDescription;
  pChannelsNonEmpty : [] ≠ pChannels;
  pPacking          : channelLayoutPacking;
  pInvariants       : channelDescriptionsBitsTotal pChannels = channelLayoutPackingBits pPacking
}.
