Previously, the implicit assumption in unification is that a boxy
type variable could never occur on both sides of the unification,
so that we'd never find 
	bx5 :=: bx5

But the pre-subsumption stuff really means that the same variable
can occur on both sides.  Consider
	forall a. a->Int <= bx5->Int
Then pre-subumption will find a->bx5; and the full subsumption step 
will find bx5:=bx5.

However, I think there is still no possiblity of a full occurs-check
failure; that is, 
	bx5 :=: Tree bx5
Although I can't quite see how to prove it!  So I've added a
DEBUG test in uMetaVar to check for this case.