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