section ‹the datatype of finite lists› theory List imports HOL.Sledgehammer HOL.Lifting_Set Zip_Benchmarks_Setup begin text ‹Note: this benchmark file is an adjusted copy of HOL.List from the standard distribution (dated 07.11.2025)›