proposition: Lemma TupleToListW_length: forall (N : nat) (tuple : FiatWTuple N), Datatypes.length (TupleToListW tuple) = N.
proof: Proof. induction N; intros. - destruct tuple; reflexivity. - simpl; f_equal; apply IHN. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics