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