Theorem channelLayoutDescriptionBitsDivisible8 : forall (c : channelLayoutDescription),
  divisible8 (channelLayoutDescriptionBits c).
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
