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
}