Update to the current version of the up-to development.

This is in response to the fossacs14 reviews.

It no longer relies on the lax_coinduction, which will soon be deleted.