formula_list(usable).

( all y v w ( i(k(U,n(k(y,v),w)),k(U,n(k(r(y),w),v))) )).

( all y v w ( i(k(U,n(k(r(y),w),v)),k(U,n(k(y,v),w))) )).

( all x y z ( k(U,n(k(x,y),z)) = k(U,n(k(r(x),z),y)) )). % (xvi)_1

end_of_list.