%lemmaP1

lemmaP1(S,T,I) == ((0=<I and pbeta(S,T)) => pbeta(lift(S,I),lift(T,I))).