use(subst).
use(int).
use(eta).
use(int_lemmas).
use(subst_lemmas).
use(lemmaE2).

lemmaF1(S,T,U,I).     %noetig

(~free(var(j),0) => lemmaE2(abs(app(var(j),var(0))),subst(var(j),0,u),v,i)),

((eta(s,t) and all(I,lemmaE2(s,t,u,I))) =>
  all(J,lemmaE2(app(s,v),app(t,v),u,J) and lemmaE2(app(v,s),app(v,t),u,J))),

((eta(s,t) and all(I,lemmaE2(s,t,u,I))) =>
  all(J,lemmaE2(abs(s),abs(t),u,J))) -> [].

top_predicates_precedence([lemmaE2]).
option([var_overlaps(off),search_depth(1)]).
:-sarp(+[15]),saci([2]).