eta(A,B) -> eta(abs(A),abs(B)).
eta(A,B) -> eta(app(A,C),app(B,C)) .
eta(A,B) -> eta(app(C,A),app(C,B)) .
eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0).
lemmaE8(A,B,C)==(eta(A,B)and eta(A,C)=>exists(D,(D=B or eta(B,D))and(D=C or eta(C,D)))).
lemmaE2(A,B,C,D)==(0=<D and eta(A,B)=>eta(subst(A,D,C),subst(B,D,C))).
lemmaE1(A,B,C)==(0=<C and eta(A,B)=>free(B,C)<=>free(A,C)).
lemmaE1(A,B,C) .
lemmaE2(A,B,C,D)  .
~free(s,0)=>lemmaE8(abs(app(s,var(0))),subst(s,0,u),subst(s,0,u)),~free(s,0)and eta(s,t)=>lemmaE8(abs(app(s,var(0))),subst(s,0,u),abs(app(t,var(0)))),eta(s,t)=>(eta(s,x)and lemmaE8(s,t,x)=>lemmaE8(app(s,u),app(t,u),app(x,u))and lemmaE8(app(u,s),app(u,t),app(u,x)))and(eta(a,b)=>lemmaE8(app(s,a),app(t,a),app(s,b))and lemmaE8(app(a,s),app(a,t),app(b,s))),eta(s,t)and eta(s,x)and lemmaE8(s,t,x)=>lemmaE8(abs(s),abs(t),abs(x)) ->  [].