proposition: Lemma CompPreservesFilterMethod: forall r inp, refine (FilterMethod myh mytopkt mytotup r inp) (FilterMethod_Count myh mytopkt mytotup r inp).
proof: Proof. prove_count_refine. 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 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields