fact: Record ipv4_input_pkt := { ipv4_len : N; ipv4_id : N; ipv4_df : bool; ipv4_mf : bool; ipv4_fragment_offset : N; ipv4_ttl : N; ipv4_protocol : N; ipv4_source : N; ipv4_dest : N }.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core