Previously, manifest fields constrained a record's values. Now, the
record value doesn't contain the manifest field at all. Instead, the
manifest value is placed on the projector frame by the elaborator when
appropriate.

This change also fixes a bug in Inversion where the running record
prefix was extended at the wrong time.

This change fixes a further bug in Environment.resolveLocal(name:) where
the field spec closure was being instantiated with a full record instead
of a truncated one.

This includes many further refactorings.

Swift's overloading is really dangerous LOL... I thought this was
dispatching to ReversedCollection, but it is actually using
Sequence.reversed(), which is linear time.

Unfortunately, the unifier still does. In the case for records, we need
to put a coercion in case of a postponement, but in order to do a
coercion we need to know the type of the field.

Following my blog post: https://www.jonmsterling.com/01KN/

What isn't working yet is:

The local "dubbings" are blown away when abstracted to a global goal
via Environment.antecedents. This needs to be kept in the goal type
somehow.

Eta-contraction should make you cringe, but it's actually needed for a
number of things. We need to know if something is equal to a local
variable (in order to rename the goal) and later on we will need the
same in order to implement the SUBST rule from Elimination With A
Motive.

I have been very careful to ensure that this version of eta contraction
is actually type-safe *and* fully general, unlike the one in Agda ;-)

I don't know why I didn't see before that I could use the partial
substitution action already for this.

This is achieving what I did before by means of a normalisation
round-trip. The key thing is that the partial substitution application
forces at every level.

I am not completely certain that this is entirely fixed, as my comment
indicates. It may be wise in the future to add a routine to actually
*verify* that the resulting quoted term does not refer to any former local
variables outside the scope.

An alternative solution may be to *keep* the old local scope around, and
to extend it only. We would just remove all the local names from the old
scope so that they do not pollute the user's view.

The bindings come from context \Gamma, so they must be reindexed before
they can be used.

A child unifier is necessary for (1) backtracking, and (2) keeping track
of whether postponed metas were introduced to decide whether to insert a
coercion.

This will obviate many instances of child environment.

This particular use of hierarchical names was getting annoying for a few
reasons.

1. It was not guaranteed to be unique.
2. The names were too long to be shown in output, and were not useful in
debugging in practice because they were like [...,body,body,body,...].

The new approach is easier to deal with and will make it possible to
decrease the amount of child environments used in the system.