Lemma channelLayoutDescriptionBitsAdd : forall d ds,
  channelDescriptionsBitsTotal (d :: ds) =
    (cdBits d) + (channelDescriptionsBitsTotal ds).
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
