formula_list(usable).

(	all x y ( k(n(k(x,y),I),U) = k(n(x,r(y)),U) )). % (xxi)

end_of_list.