fact: Record FilterAdapter (f: FilterType) := { h: Heading; topkt: @Tuple h -> input; totup: input -> @Tuple h; thm: Complete_Dropped_equiv h topkt totup f }.
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