%lemmaE1

lemmaE1(S,T,I) == ((0=<I and eta(S,T)) => (free(T,I) <=> free(S,I))).