formula_list(usable).

( all x y ( U = Z -> x = y )). % (xxxiii)

end_of_list.