Interesting! Two questions:
1) Could you maybe simplify the computational effort by defining "divide by 2" instead of general division, since you only ever divide by 2 for Collatz?
2) The author concludes by explicitly checking each integer. Given the power of types, isn't there a single statement you can make that would prompt it to check all integers, i.e. seeing if it can prove that all integers type-check?
