fact: Definition Complete_Dropped_qs_equiv {h: Heading} (totup: input -> @Tuple h) (r_o: UnConstrQueryStructure Complete_PacketHistorySchema) (r_n: UnConstrQueryStructure (PacketHistorySchema h)) := forall inp idx, ((r_o!"History") {| elementIndex := idx; indexedElement := (Complete_totup inp) |} -> (r_n!"History") {| elementIndex := idx; indexedElement := (totup inp) |}) /\ ((r_n!"History") {| elementIndex := idx; indexedElement := (totup inp) |} -> exists inp', (r_o!"History") {| elementIndex := idx; indexedElement := (Complete_totup inp') |} /\ totup inp' = totup 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