%lemmaE7

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

%top_predicates_precedence([lemmaE7]).