Yes, my argument relies on immutability of all values (including `increase`). Also, under lazy evaluation we can call `adjust2` immediately, since we know it's a `lambda`; yet attempting to call `adjust1` will force evaluation of `increase`; not good if `increase = provable(collatz_conjecture)`!