fact: Definition IndexedElement_ListWToTuple (element: @IndexedElement (list W)) : FiatWElement (List.length (indexedElement element)) := {| IndexedEnsembles.elementIndex := element.(elementIndex); IndexedEnsembles.indexedElement := ListWToTuple element.(indexedElement) |}.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics