This post doesn't seem to be getting much attention, so I thought I'd ask again here.
What is it about the type CR that causes this? How can the postcondition be modified to allow SPARK to prove this?
And why do I need to enter at least 220 characters?
As shown in the comments, using --level=1 proves this.