This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be

This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf. Edit: I found an explanation https://ionathan.ch/2021/08/04/sized-types.html https://ionathan.ch/2021/08/04/sized-types.html