%lemmaE2

lemmaE2(S,T,U,I) == ((0=<I and eta(S,T)) => eta(subst(S,I,U),subst(T,I,U))).