fact: Definition Complete_Dropped_equiv (h: Heading) (topkt: @Tuple h -> input) (totup: input -> @Tuple h) (f: FilterType) := forall r_o r_n, Complete_Dropped_qs_equiv totup r_o r_n -> forall inp, refine (Complete_filter f r_o inp) (f h topkt totup r_n inp).
imports: Bedrock.Word Coq.Vectors.Vector IndexedEnsembles Fiat.Common.ilist2 Fiat.Common.EnumType Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables IPTables