n:
, f:(n
(x,y:3*//(x LangOf(auto3_3())-induced Equiv y))).
Bij(n; x,y:3*//(x LangOf(auto3_3())-induced Equiv y); f)
auto3_3_minimization
s,a. a),0,(s.true
) >
Thm* n:, f:(n(x,y:3*//(x LangOf(auto3_3())-induced Equiv y))).
Bij(n; x,y:3*//(x LangOf(auto3_3())-induced Equiv y); f)
auto3_3_minimization