[Haskell-cafe] Proof question -- (==) over Bool

[R J]

I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:
(==)                       :: Bool -> Bool -> Boolx == y                     =  (x && y) || (not x && not y)
My question is:  are the proofs below for reflexivity and symmetricity rigorous, and what is the proof of transitivity, which eludes me?  Thanks. Theorem (reflexivity):  For all x `elem` Bool, x == x.
Proof:
      x == x  =    {definition of "=="}      (x && x) || (not x && not x)  =    {logic (law of the excluded middle)}      True
Theorem (symmetricity):  For all x, y `elem` Bool, if x == y, then y == x.
Proof:
      x == y  =    {definition of "=="}      (x && y) || (not x && not y)  =    {lemma:  "(&&)" is commutative}      (y && x) || (not x && not y)  =    {lemma:  "(&&)" is commutative}      (y && x) || (not y && not x)  =    {definition of "=="}      y == x
Theorem (transitivity):  For all x, y, z `elem` Bool, if x == y, and y == z,then x == z.
Proof: ? 		 	   		  
_________________________________________________________________
Hotmail has tools for the New Busy. Search, chat and e-mail from your inbox.
http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_1
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100521/07b7eff7/attachment.html