(certify-book "basic-examples" 0 t :ttags (my-ttag))