~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)).

% should go into a separate file:
%etas(S,S).

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

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

precedence([free,subst,etas,eta,app,abs,var]). %hg