some progress satisfying the obligations of diff

... in some of the most ugly proving ever. and with
still three dicey obligations to go.

which means that size.v doesn't yet compile