plus :: (n m::nat | n + m < 2^32) : nat -- (1)
plus :: (n m::nat) : nat                -- (2)

plus 1 2 -- pretty sure it chose (1)
plus 1 2^67 -- pretty sure it chose (2)

if n < 2^30:
	plus n n -- not sure, but more likely (1)

if n < 2^30:
	plus n (n + 2^29) -- not sure for this one at all