HOL.Limited_Sequence