fact: Definition In_History_Constr {h} totup (r: QueryStructure (PacketHistorySchema h)) (pre: input) := IndexedEnsemble_In (GetRelationBnd r {| bindex := "History"; indexb := _ |}) (totup pre).
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