fact: Definition dhcp_request_input : input := must (input_of_bytes FORWARD (bytes_of_ByteBuffer dhcp_request)).
imports: Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.Ports Coq.Vectors.Vector