Not really the ideal solution, but helpful. It'd be nice to record all
the data and be able to expand after the fact.

Instead of having "fallback clauses" to handle projection, we now
have `ProjectionEq(<T as Trait>::Bar = U)`, which can be proven
either by normalizing *or* by skolemizing.

This required adjusting how we handle elaboration. That is, we now
"expand" a `T: Trait<Bar = U>` (which is the user syntax for projection
equality) into `T: Trait` as well, which in turn expands into `WF(T:
Trait)`. We do this instead of having a clause like:

> `(T: Trait) :- exists<U> { (T: Trait<Bar = U>) }`

This is because that clause caused issues for the recursive solver; in
particular, `exists<U> { (T: Trait<Bar = U>) }` always resolves to an
ambiguous result, since there is no unique `U`.

This PR adjusts the tests appropriately. Mostly we add normalize and
projection. In a few cases, the SLG solver doesn't work yet; those are
tagged with FIXME (and fixed in a later commit).

This is not only more efficient, but it also sidesteps the problems that
led to the SLG solver recursing infinitely when unifying goals involving
projections.

This also uncovers a potential flaw with the truncation operation, in
that it does not concern itself with internal binders. For example, we
might truncate a type like `for<'a> fn(Vec<&'a u32>)` into `for<'a>
fn(?X)`. This is problematic because there is no value of `?X` that
could reference `'a`. For now, the SLG solver will panic in this
scenario, but probably truncation needs to truncate the binder as well.