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:W...