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