[prover] `$Arbitrary'T'` needs to distinguishes its instances

[wrwg]

The current way how $Arbitrary'T' is implemented creates an unknown but fixed value of the given type. However, this is unsound, since different uses of this constant in the same verification should be allowed to have different values.

What we need here is to identify the syntactic instances, as done with the translation of choose, where the source location is used to distinguish instances.

[github-actions]

This issue is stale because it has been open 45 days with no activity. Remove the stale label or comment - otherwise this will be closed in 15 days.