Changed lots of = to \id and some to \defeq because there were some wrong uses of =. Also there were some typos in the proof of associativity