A proper lazy list has a spine exposing either finitely many cons constructors followed by
[], or infinitely many cons constructors, without an undefined tail at a finite position. This is a condition on the spine: an element may itself be the bottom value without hiding the list's constructors. A partial list with a finite visible prefix followed by fails this condition. The distinction supports productivity proofs that inspect constructors without evaluating the stored elements. New to topics? Read the docs here!