[Haskell-cafe] Proof format

[R J]

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:WL:en-US:WM_HMP:042010_2
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100519/917799cb/attachment.html