Lambda functions should be supported by the tool. This needs a level of indirection to avoid non-termination issues. This can be achieved by shoving their runtime reps (which is going to be HList Tp.denote argTypes -> Expr Tp.denote outType) onto the heap and pass them around in references.

AST, syntax and semantics need to be extended to support lambda calls.

A good test case for this would be a module that

1. Defines Slice.reduce
2. Calls it with e.g. a lambda that adds numbers
3. The postcondition that this is a sum of all items in the slice should be provable with all hoare-logic steps skipped by automation (steps and sl)