fact: Definition udp_input_pkt_of_pkt pkt := {| udp_source_port := wordToN pkt.(UDP_Packet.SourcePort); udp_dest_port := wordToN pkt.(UDP_Packet.DestPort); udp_payload := pkt.(UDP_Packet.Payload) |}.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core