Am Samstag, 14. März 2009 22:44 schrieb Marcin Kosiba: > > (L) forall u v w. (u - v) - w = (u - v) - w > > Typo? :) > > (L) forall u v w. (u - v) - w = (u - w) - v > Sure. Thanks for spotting it. I had (x-y)-z = (x-z)-y first, then decided it would be better to use different variable names...