use(int).

I<K -> lift(var(I),K) = var(I).
K=<I -> lift(var(I),K) = var(s(I)).

lift(app(S,T),K) = app(lift(S,K),lift(T,K)).

lift(abs(S),K) = abs(lift(S,s(K))).


K<I -> subst(var(I),K,S)=var(p(I)).
       subst(var(I),I,S)=S.
I<K -> subst(var(I),K,S)=var(I).


subst(app(T,U),K,S)=app(subst(T,K,S),subst(U,K,S)).

subst(abs(T),K,S)=abs(subst(T,s(K),lift(S,0))).

precedence([subst,lift,app,abs,var,s,p,0]).