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
is an expression in Dafny. Semantically, it is the same as
, but the lemma is used when verifying the well-formedness of