[nightlyherb]

Using church numerals[1],

  right_incr(n)  =
    g => y => n(g)(g(y))

and using the following shorter fixed-point combinator[2],

  X(f) =
    ( a => a(a) )( x => f(x(x)) )

I get this junk:

  X(right_incr)
    = ( a => a(a) )( x => g => y => x(x)(g)(g(y)) )
    = ( x => g => y => x(x)(g)(g(y)) ) ( x => g => y => x(x)(g)(g(y)) )

  X(right_incr)(g)(y)
    = let f = ( x => g => y => x(x)(g)(g(y)) )
      in f(f)(g)(y)
    = let .. in f(f)(g)(g(y))
    = let .. in f(f)(g)(g(g(y)))
    = ...

Which, as you can see, only gets more complex when I try to transform it.

[1] https://en.m.wikipedia.org/wiki/Church_encoding [2] https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other...