Sometimes it is hard to use a normal Dafny method lemma where you need it. For example, if you want to use a lemma inside a function or in a contract. There is a simple solution.

Given a method lemma:

static lemma SomethingValid(s:S) requires P(s); ensures Q(s); |

We can produce a function lemma:

static lemma SomethingValidFn(s:S) requires P(s); ensures Q(s); ensures SomethingValidFn(s); { SomethingValid(s); true } |