On 23/01/2019 13.26, Henning Basold wrote: > But you don't refer to sized types, do you? No, size-change termination: https://en.wikipedia.org/wiki/Size-change_termination_principle -- /NAD