Still for some reason trying to find a nice closed form for (1 + D + D 2 + ...)T for various T, but not succeeding. Increasingly confident that substitution inversion is the right place in higher-order unification to start thinking about types and label refinements. The formalism is still pretty tricky though.