Extend run meta to support trailing lambdas

[TurtlePU]

A common pattern in Arend proofs (apart from ==< equalities >==) is a sequential invocation of functions and metas. A run meta makes these chains comprehensible as can be seen here and here.

However, several ubiquitous callables such as path and function extensionality expect a function as their last argument. This last argument often ends up being a lambda which itself consists of invocations which can be stacked inside run block. This might lead to something known in JS as "callback hell":

run {
    lemma1,
    path,
    \lam i => run {
        lemma2,
        ext,
        \lam x => run {
            ...
        }
    }
}

I propose to extend run meta with a <- arrow similar to do-notation in Haskell to escape this callback hell:

run {
    lemma1,
    i <- path,
    lemma2,
    x <- ext,
    ...
}

(One could use a <= arrow instead for consistency with => arrow, but fat left arrow is already used as less-than-or-equals sign)

To be precise, a <- arrow separates a new identifier <id> and an arbitrary expression <e>. After run invocation, all statements after <--statement are put inside a lambda <l> supplied as an argument to <e>; argument of <l> is called <id>.

Note that this also composes nicely with __:

run {
    x <- takesLambdaAsFirstArgument __ arg2 arg3
    ...
}

[TurtlePU]

On the second thought, what to do with trailing lambdas of several arguments? Write down a space-separated list?

run {
    x y <- \new Embedding f
    ...
}