Regarding my earlier question to the group, I notice that my problem was in my definition of commutative. It should include universal quantifiers to bind the variables on the rhs. commutative(f) <=> \A e \A e' (f ! [e, e'] = f ! [e', e]) Of course this is what I really want, since otherwise I'd be able to show f commutative if it commuted for any two inputs. Sorry to waste other's time. - Mitch