[Agda] Questions about unification

[Roman]

András, it's been a while since I studied HOU, so I might forget some
things, especially terminology. However this equation

    U [x, y, w, w] =?= App (Var x) (Var w)

can be transformed into (assuming the type of `w` doesn't depend on `y`)

    U [x, _, w, w] := V [x, w, w]
    V [x, w, w] =?= App (Var x) (Var w)

And if you have a flexFlex case like in Ulf's example, then I don't
see why you can't prune unused variables on both sides of the
equation.