shminux comments on Towards formalizing universality