fact: Definition cond_dstport port : condition input := let fn := tcp_or_udp tcp_dest_port udp_dest_port in fun pkt => Neqb pkt.(fn) port.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core Coq.Vectors.Vector