formula_list(usable). % double complement law, and a corollary of it

	( all x ( c(c(x)) = x )). % 15

	( all x y ( u(x,y) = y -> c(u(y,c(x))) = Z )). % 16a

	( all x y ( c(u(y,c(x))) = Z -> u(x,y) = y )). % 16b

end_of_list.