Consider the TRS R consisting of the rewrite rule

1: app(app(app(uncurry,f),x),y) -> app(app(f,x),y)

There are 2 dependency pairs:

2: APP(app(app(uncurry,f),x),y) -> APP(app(f,x),y)
3: APP(app(app(uncurry,f),x),y) -> APP(f,x)

Consider the SCC {2,3}.
By taking the polynomial interpretation
[uncurry] = 1
and [app](x,y) = [APP](x,y) = x + y + 1,
the rules in {1-3}
are strictly decreasing.
Hence the TRS is terminating.