formula_list(usable).

(	all x y z ( k(x,u(y,z)) = u(k(x,y),k(x,z)) )).	 % (v)_1

(	all x y z ( k(u(x,y),z) = u(k(x,z),k(y,z)) )).	 % (v)_2 == BV

end_of_list.