formula_list(usable).  % inclusion between relations

	all x y ( i(x,y) <-> ( u(x,y) = y ) ).

end_of_list.