formula_list(usable). % simplicity axiom % inessential, unused, possibly useful in some cases all x ( x = Z | k( k( U, x ), U ) = U ). end_of_list.