Check termination of recursive functions

[jespercockx]

We eventually want to check that functions are terminating, but ideally without adding a whole termination checker to the trusted code base. Instead, we could have a set of judgements for reasoning and proving about sizes of arguments, similar to what is proposed in agda/agda#7152.