Make the setoid equivalence and metric for excl and csum independent from the chosen OFE
Up to now, these 4 inductives syntactically depend on the OFE, so that we cannot rewrite an equality using (ofe_equiv (cmra_ofe (exclR ....))) if we only have proper instances for (ofe_equiv (exclC ...)).
We can solve this problem by doing these changes. Is there any reason why we did not do that before ?
PS : This branch follows jh/cancellale for convenience (in Lambdarust). I can rebase it on master or anything else if needed.