fact: Definition bytes := { n: nat & ByteBuffer.t n }.
imports: BinNat Coq.Lists.List Bedrock.Word Fiat.Common.EnumType Fiat.Narcissus.Formats.ByteBuffer Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.UDP_Packet Fiat.Narcissus.Examples.NetworkStack.TCP_Packet