Generalize eqfun and eqrel to dependent functions

[Tragicus]

Motivation for this change

Generalizes eqfun and eqrel to dependent functions (which will be useful when we will want and be able to put instances on dependent function types). This changes the implicit arguments of _ =2 _ since now, in (f =2 g) x y, x appears in the type of y.

Minimal TODO list

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers
• tried to abide by the contribution guide
• this PR contains an optimum number of meaningful commits

See this Checklist for details.

Overlays

• Another way to adapt to math-comp#1300 rocq-community/fourcolor#66
• Adapt to mc#1300 rocq-community/tarjan#27

Automatic note to reviewers

Read this Checklist.

[CohenCyril]

You could add an Arguments directive to preserve the former implicits. I think in this particular case I'd rather put one _ to omit a redundant argument in the dependent case rather than use @ and put many _ in the non-dependent case...

[Tragicus]

I can not access x to make it explicit without changing the type of eqrel _ _, which would break things very hard. rocq-prover/rocq#13435 seems to imply that this issue is by design (see also this Zulip thread)