formula_list(usable). % echo of lemmas proved earlier

( all x z (u(x,I)=I->u(k(x,z),z)=z) ).

( all x y z (i(x,y)->i(k(z,x),k(z,y))) ).

( all x y (n(x,y)=n(y,x)) ).

( all x y i(n(x,y),y) ).

( all x y z (i(x,y)->i(n(z,x),n(z,y))) ).

( all x (k(I,x)=x) ).

( all x y z ( i(x,y) -> i(k(x,z),k(y,z)) )). % (vii)_1

end_of_list.