I tried to implement the lambda calculus successor function on my own, but it's different from the Wikipedia entry on Church encoding. The entry wraps the 'b' around the rest of the expression after injecting the 'c', whereas I tried injecting 'b's application on 'c'. Is there a fundamental difference between these two expressions, and what would be good practice when writing this stuff down?
increment = (λa.λb.λc.((a b) (b c)))
increment = (λa.λb.λc.(b ((a b) c)))
This is after I alpha-reduced to 'a', 'b', and 'c', so the article is different.