proposition: Lemma TupleToListW_length': forall (N : nat) (tuple : FiatWTuple N), BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> Datatypes.length (TupleToListW tuple) = Word.wordToNat (Word.natToWord 32 N).
proof: Proof. intros; rewrite Word.wordToNat_natToWord_idempotent by assumption. auto using TupleToListW_length. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics