Suggestion: let expressions

I'd like to suggest a small tweak to help writing code. The default application rule for pure type systems is as follow:

```
L |- f: \/(x: A).B L |- a: A
-------------------------------------
L |- (f a): B[a/x]
```

I.e., both the function abstraction and the parameter have to be typeable on their own. My suggestion is to allow a let-expression within the language, with the following rule:

```
L |- a: A L |- b[a/x]: B
---------------------------------
(let x = a in b): B
```

I.e., it first typechecks the "parameter", then beta-reduces the body, and only then checks the body of our "function". This extension keeps the calculus of constructions consistent, but makes it a bit more expressive, and it would allow to do things that now require Morte to load the expression from another file.

To avoid adding keywords, I'd suggest square brackets for Morte's syntax for that. E.g.,

```
[Nat = \/(N: *).\/(Z: N).\/(S: N -> N).N]
\(n: Nat) ->
n
```

And it would work as if we had a file `./Nat` with that definition. What do you think?

The issue names no repository files or tests, but proposes a new Morte let-expression and square-bracket syntax to replace some separate-file loading. Start by locating the parser, type-checking, and file-loading entry points, then establish the syntax and typing behavior; done means the feature is implemented consistently with the proposed rule.

Written by the indexing model from the issue text.