1    λ(a : Type)
2  → λ(y : a)
3  → λ(xs : ./Type a)
4  → (./../Function/category).compose
5    (List a)
6    (List a)
7    (List a)
8    (λ(ys : List a) → [ y ] # ys)
9    xs