Syntactic sugar for lemma functions
The following syntactic sugar for automatically introduce proof-based lemma functions:
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
This automatically generates:
let [rec] lemma a'apply xs requires { hs } ensures { p } [variant {v}] = begin t end
[with …]