formula_list(usable).

(	all x ( ( k(x,U)=U )  -> i(I,k(x,r(x))) ) ). % (xx)_a

(	all x ( ( k(x,U)=U ) <-> i(I,k(x,r(x))) ) ). % (xx)

end_of_list.