Everything involving only catamorphisms (|...|) terminates, since all atoms in the language define terminating functions, and least fixed point types can only b

Everything involving only catamorphisms (|...|) terminates, since all atoms in the language define terminating functions, and least fixed point types can only be constructed in finite ways using the 'in' function or by catamorphism themselves, so are necessarily finite.