proposition: Lemma OutgoingToImpliesOutgoing: forall inp dst, (OutgoingToRule dst).(cf_cond) inp -> OutgoingRule.(cf_cond) inp.
proof: Proof. intros. simpl in *. unfold combine_conditions in *. apply andb_prop in H. destruct H. rewrite H. constructor. Qed.
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles