Extend `run` meta to support trailing lambdas

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](https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Ring/Solver.ard#L81) and [here](https://github.com/JetBrains/arend-lib/blob/master/src/Category/Sub.ard#L50).

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 `` and an arbitrary expression ``. After `run` invocation, all statements after `<-`-statement are put inside a lambda `` supplied as an argument to ``; argument of `` is called ``.

Note that this also composes nicely with `__`:

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

Start by reading the existing run usage in src/Algebra/Ring/Solver.ard and src/Category/Sub.ard, then compare those examples with the proposed trailing-lambda syntax. Done means run accepts the `<-` form, nests subsequent statements in the supplied lambda, and composes with `__` as described.

Written by the indexing model from the issue text.