Answering my own question

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