Change in relevances for apps and vars as doc'ed.

This was supposed to fix the incorrect unification between arrow relevance
of yet unknown arrow types and their arguments.

The simplest example where this shows up is twice:
twice f x = f (f x)

Here f has a type of (a -> a) with an arrow relevance of some beta value.
twice has to have that same beta for the last arrow, but it did not because
x had a fresh type from the abstraction rule.

While the current changes seem to fix in theory, in practice we need to further
develop the lattices since context splitting sometimes faces these betas (whoops)
so I should stop delaying that any further.