In Dafny do function expressions not generate closures?
It does, but an important part of the language is top-level function
_expression_ definition, which would not have a lifting target.
So yes, choice-filters-to-apply seems like a solution, but see my above question about how to use it properly.
Thanks!