Module and elim

[thomas-lamiaux]

@felixwellen realized last week that there is files such as the Free comMonoid or Direct Sum that define a named module with one function f. So one need to call Elim.f X Y Z x y z which is more complicated and not very clear. I think we decided that it should be done by replacing the module name by _ and f by the module name ?

Maybe this should be the object of specific PR and a note somewhere in naming with #823

[felixwellen]

I agree that it would be good to change all instances of that in a PR.