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