formula_list(usable).

( all x y ( x = y <-> u(n(x,y),n(c(x),c(y))) = U )). % (xxxii)

end_of_list.