formula_list(usable).

( all x y ( k(c(x),c(r(y))) = Z <-> i(k(U,c(x)),y) )).

( all x y ( c(k(c(x),c(r(y)))) = U <-> i(k(U,c(x)),y) )).

( all  x y ( i(x,y) <-> u(c(x),y) = U )).

( all x y ( c(k(c(x),c(r(y)))) = U <-> u(c(k(U,c(x))),y) = U )).

end_of_list.