formula_list(usable). % Schroeder equivalences

	( all x y z ( i(k(x,y),c(z)) <-> i(k(r(x),z),c(y)) )). % (xii)_1

	( all x y z ( i(k(x,y),c(z)) <-> i(k(z,r(y)),c(x)) )). % (xii)_2

end_of_list.