Propagate `requires` in lambda functions in Dafny

Question

How do I prove something about the assumption of a lambda function? I would like to prove the following

lemma propagate_requires(f: int --> int,y:int)
ensures ((x: int) requires f.requires(x) => f(x)).requires(y) == f.requires(y)

This should be obviously true from my understanding. However, Dafny does not propagate the assumption.

How are these requires actually handled by Dafny?

Answer 1

It is verifiable in one direction but not in opposite direction. This verifies

lemma propagate_requires(f: int --> int,y:int)
  ensures ((x: int) requires f.requires(x) => f(x)).requires(y) <== f.requires(y)
{}

This does n't verify

lemma propagate_requires(f: int --> int,y:int)
  ensures ((x: int) requires f.requires(x) => f(x)).requires(y) ==> f.requires(y)
{}

There is issue related to this https://github.com/dafny-lang/dafny/issues/2137.