%lemmaB3a

lemmaB3a(S,T,X) == (betas(S,T) =>
                    (betas(abs(S),abs(T)) and
                     betas(app(S,X),app(T,X)) and betas(app(X,S),app(X,T)))).