The only drawback is that we have to restrict iprod to finite types,
but that is fine.

Thanks to Amin Timany for the suggestion.

Most notably, there is no need to internalize stuff into the logic
as it follows from generic lemmas for discrete COFEs/CMRAs.

This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.