f.requires forgotten for f defined with requires clause

[erniecohen]

Dafny version

4.10

Code to produce this issue

predicate p(x:int)
const f := (x:int) requires p(x) => x
lemma test(x:int) ensures f.requires(x) ==> p(x) {}

Command to run and resulting output

What happened?

This should verify. (Note that the reverse implication does.)

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

Mac