formula_list(usable). ( all x y ( ( i(k(r(x),x),I) & (k(x,U)=U) ) -> ( c(k(x,y))=k(x,c(y)) ) )). % (xxx)_1 end_of_list.