fact: Definition fiat_ipv4_protocol_to_enum (proto: fiat_ipv4_protocol) : EnumType ["ICMP"; "TCP"; "UDP"] := match proto with | ICMP => ```"ICMP" | TCP => ```"TCP" | UDP => ```"UDP" end.
imports: Fiat.Narcissus.Examples.NetworkStack.TestInfrastructure Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Strings.String Fiat.Common.EnumType