fact: Definition ipv4_decode (bs: bytes) := WrapDecoder (@IPv4_decoder_impl) bs.
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