389710 (1) [Avatar] Offline
#1
There is a typo in the predicate `Last` which makes the definition impossible to complete.

The type of the `LastOne` constructor should be `LastOne [value] value`, otherwise pattern matching on the constructor causes
no refinement and makes it impossible to discharge the necessary proof obligations.
Edwin Brady (65) [Avatar] Offline
#2
So it is, thanks for noticing! I've fixed it for the next version.