%lemmaE6

lemmaE6(S,T,I) == ((0=<I and eta(S,T)) => eta(lift(S,I),lift(T,I))).

%top_predicates_precedence([lemmaE6]).