%lemmaE3b

lemmaE3b(S,T,U,V) == (etas(S,T) => (etas(U,V) => etas(app(S,U),app(T,V)))).