Unable to assert quantification over map comprehension

[ssomayyajula]

Dafny version

latest

Code to produce this issue

type Msg = int

datatype Type =
| Send(next: map<Msg, Type>)
| Recv(next: map<Msg, Type>)
| End() {
  predicate CanSend(msg: Msg) {
    match this
    case Send(next) => msg in next
    case Recv(next) => forall msg <- next :: next[msg].CanSend(msg)
    case End()      => false
  }
}

method Main() {
  var x := Recv(map[1 := Send(map[2 := End()])]);
  // by clause verifies, but not the assert itself
  assert x.CanSend(2) by {
    forall msg <- x.next ensures x.next[msg].CanSend(2) { }
  }
}

Command to run and resulting output

dafny verify ...

What happened?

This should verify...right?

What type of operating system are you experiencing the problem on?

Mac

[ssomayyajula]

Closing because of typo + can't reproduce my issue on this smaller example