formula_list(usable).

% m selects an inclusion minimal element from its argument
%	(for definiteness, m(0)=0)

all y x ( e(y,x) -> e(m(x),x) ).
all y x ( ( e(y,x) & i(y,m(x)) ) -> m(x) = y ).
m(0) = 0.

end_of_list.