(include-book "utilities")
(certify-book "vcg-examples" 1)