Is this how a rigorous Haskeller would lay out the proofs of the following theorems? This is Bird 1.4.6. (i) Theorem: (*) x = (* x) Proof: (*) x = {definition of partial application} \y -> x * y = {commutativity of "*"} \y -> y * x = {definition of "(* x)"} (* x) (ii) Theorem: (+) x = (x +) Proof: (+) x = {definition of partial application} \y -> x + y = {definition of "(x +)"} (x +) (iii) Theorem: (-) x /= (- x) Proof: (-) x = {definition of partial application} \y -> x - y /= {definition of prefix negation, which is not a section} (- x) _________________________________________________________________ Hotmail is redefining busy with tools for the New Busy. Get more from your inbox. http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:W...