this. (IMHO the key point is that we have to stop to abuse to type > system to achieve the same notation for different operations).
I don't see why the recpower is an "abuse" of the type system... If I want to use inside a class, the type is fixed and I see no problem... This was not my point at least. I want(ed) to have merge point for the so many nice-looking classes, so that the interesting theorem can be proved inside the locale and not only inside axclasses. Amine.
