In section 11.1.4, we're implementing the function getPrefix : (count : Nat) -> InfList ty -> List ty.

A (very) minor nitpick: the type variable changes from ty to a when showing the implementation below.