Would the purpose of using it be to get the implication P(x) ==> Q(x) somewhere in the program?
How would you use it? Can you not just an ordinary lemma instead? Note that
SomeLemma(x); E
is an expression in Dafny. Semantically, it is the same as E , but the lemma is used when verifying the wellformedness of
E .
Rustan
