chapter ‹Generated by Lem from ‹misc/lem_lib_stub/lib.lem›.› theory "LibAuxiliary" imports Main "HOL-Library.Datatype_Records" "LEM.Lem_pervasives" "LEM.Lem_list_extra" "LEM.Lem_string" "Coinductive.Coinductive_List" "Lib" begin ― ‹‹**************************************************›› ― ‹‹ ›› ― ‹‹ Termination Proofs ›› ― ‹‹ ›› ― ‹‹**************************************************›› termination lunion by lexicographic_order end