proposition: Lemma TruncateList_length {A} n : forall (a: A) (l: list A), List.length (TruncateList a n l) = n.
proof: Proof. induction n, l; simpl; intuition. Defined.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics