formula_list(usable).

% e designates membership ("in")
% a designates arbitrary selection ("arb")
% w designates single el't adjunction ("with")
% l designates single el't removal	("less")

all y x ( e(y,x) -> e(a(x),x) ).
-( e(a(0),0) ).
all v x y ( e(v,w(x,y)) <-> ( e(v,x) | v = y ) ).
all v x y ( e(v,l(x,y)) <-> ( e(v,x) & -( v = y ) ) ).

end_of_list.