formula_list(usable).

(	all x ( i(x,I) -> (k(x,x) = x) ) ).  % (xxii)_2

(	all x ( i(x,I) -> (r(x)=x) ) ).      % (xxii)_1

end_of_list.