ls2(x,u) * u->v * v->w * ls2(w,y)  |- ls(x,a') * ls(a',b') * b'->y