Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod`

The title says it all.

The only remaining question is whether the iprod cmra stuff should still be in a separate file or whether it should be put into cmra.v.