(include-book "utilities") (certify-book "demo" 1)