WYIL: verification is working again in a limited fashion.  It at least verifies the simplest function involving nats.