fact: Definition IsSome {A} (x: option A) := match x with Some _ => True | None => False end.
imports: Bedrock.Word Fiat.Narcissus.Examples.NetworkStack.EthernetHeader Fiat.Narcissus.Examples.NetworkStack.ARPPacket Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Examples.NetworkStack.UDP_Packet AlignedByteString