turn lemma into lemma function automatically
I propose we turn any lemma automatically into a lemma function. (This way, we can instantiate it manually anywhere.)
Of course, there may be several ways of doing it. If for instance the lemma is
lemma L: forall x. P -> Q
then it could be either
let lemma L (x) requires P ensures Q
or
let lemma L(x) ensures P->Q
I suggest we choose the former, heuristically. If ever users want the latter, they can always introduce a dedicated lemma function.
Such a change should not impact existing proofs, as we are only introducing additional ghost functions. We could imagine having a label to tag lemma we do not want to translate into lemma functions (if ever).