fact: Fixpoint ListWToilist2 (l : list W) : ilist2.ilist2 (B := fun x => x) (MakeVectorOfW (List.length l)) := match l as l0 return (ilist2.ilist2 (MakeVectorOfW (Datatypes.length l0))) with | nil => ilist2.inil2 | x :: x0 => ilist2.icons2 x (ListWToilist2 x0) end.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics