(==)                       :: Bool -> Bool -> Bool

x == 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: ?