YES
TRS:
 {app(app(app(compose(), f), g), x) -> app(f, app(g, x))}
 RUF:
  Strict:
   {}
  Weak:
   {}
  Qed