formula_list(usable).

% choice function C:
%%	all x y ( e(x,C(y)) <-> ( exists z ( e(z,y) & x = a(z) ) ) ).

all x y ( e(x,y) -> e(a(x),C(y)) ).

all x y ( e(x,C(y)) -> ( exists z ( e(z,y) & x = a(z) ) ) ).

end_of_list.