[Moved to cafe] Christophe Poucet wrote:

Hello,

I think you look at the (.) . (.) as all being c's in the wrong way. You have to consider what will evaluate first (syntactical priority rules).

(.) . (.) === (.) (.) (.) -- a + b === (+) a b === c c c

Anyways the simplest case that this is equivalent can be seen here: 22:33 < vincenz> @pl \f g a b -> f (g a b) 22:33 < lambdabot> (.) . (.)

Writing it explicilty: (.) f g a = f (g a)

so we get (.) . (.) = \f -> (.) ((.) f) (.) . (.) f = (.) ((.) f) (.) . (.) f g = (.) ((.) f) g (.) . (.) f g = ((.) f) . g (.) . (.) f g a = ((.) f) (g a) (.) . (.) f g a = (.) f (g a) (.) . (.) f g a = f . (g a) (.) . (.) f g a b = f . (g a) $ b (.) . (.) f g a b = f ((g a) b) (.) . (.) f g a b = f (g a b)

Thanks for the proof. I see it's got the advantage over mine that it doesn't need to use eta expansion and is also much clearer. Regards, Brian.