proposition: Lemma ListWToTuple_Truncated_id n l : List.length l = n -> l = TupleToListW (ListWToTuple_Truncated' n l).
proof: Proof. intros; subst. unfold ListWToTuple_Truncated'. induction l. trivial. simpl. destruct (TruncateList_length (Datatypes.length l) (Word.natToWord 32 0) l). rewrite IHl at 1. reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics Fiat.ADT.Core