% eta reduction
~free(S,0) -> eta(abs(app(S,var(0))),subst(S,0,U)).

eta(S,T) -> eta(app(S,U),app(T,U)).

eta(S,T) -> eta(app(U,S),app(U,T)).

eta(S,T) -> eta(abs(S),abs(T)).

%etas(S,S).

%eta(S,T) -> etas(S,T).

% etas(S,T), eta(T,U) -> etas(S,U).

precedence([eta,free,subst,abs,app,var,0]).
top_predicates_precedence([etas]).
option(var_overlaps(off)).