%comm_lemma

comm_lemma(S,T,X) == ((beta(S,T) and eta(S,X))
                  => exists(Z,(etas(T,Z) and betar(X,Z)))).