can't label forall-ensuring statement

[kjx]

Summary

I can write assert FOO: forall x <- X :: Assertion...x... by { Proof...x... }

but I don't seem to be able to label the "equivalent"

forall x <- X ensures Assertion...x... { Proof...x... }

Background and Motivation

writing dafny

Proposed Feature

allow labels somewhere on the forall ensures version. probably after "ensures"

Alternatives

put it on the list of the other fixes to do with forall & assert by