(certify-book "stobj" ? t :ttags :all)