formula_list(usable).

(	all x ( k(k(U,r(x)),U) = k(k(U,x),U) ) ). % (xvii)_2

(	all x ( r(k(k(U,x),U)) = k(k(U,x),U) ) ). % (xvii)_3

end_of_list.