formula_list(usable).

( all x y ( ( i(k(r(x),x),I) & (k(x,U)=U) ) -> ( c(k(y,r(x)))=k(c(y),r(x)) ) )). % (xxx)_2

end_of_list.