SPARK Functional-Correctness Proof

Question

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?

Answer 1

As shown in the comments, using --level=1 proves this.