Thm* n:, f:(n(x,y:2*//(x LangOf(Auto4)-induced Equiv y))). Bij(n; x,y:2*//(x LangOf(Auto4)-induced Equiv y); f) auto4_minimization