fact: Definition TupleToListW_indexed {N} (tup: FiatWElement N) := {| TuplesF.elementIndex := IndexedEnsembles.elementIndex tup; TuplesF.indexedElement := (TupleToListW (IndexedEnsembles.indexedElement tup)) |}.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics