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