formula_list(usable).

(	all x ( k(x,I) = x) ).	% (ix)_1 == BVI

end_of_list.