Since the const tree is the same for different chunks of the same program, we can cache it when proving.