Correctly implement δ-resolver lift for modules.

[ppedrot]

Module δ-resolvers are morally a kind of substitution, associating a canonical name to some aliased constant. Functors and module types are function-like w.r.t. to resolvers, insofar as the name they introduce is bound and should be left alone. This is similar to the λ-calculus equation (λt){σ} ≡ λ(t{σ↑}) where substitutions must be lifted when going under a context.

Unfortunately, the resolver mechanism is not based on De Bruijn indices but names, and the implementation was implementing the lift in a broken way, by adding the trivial equivalence p ↦ p for some bound path p. As is expected, this does not play well with the usual algebraic operations one expect to apply to resolvers, leading to interesting breakage of invariants here and there. It did not seem enough to prove False though, just random anomalies and incompletenesses.

We fix this mess by introducing an explicit lift operation in δ-resolvers which is handled specifically by substitution. En passant, the internals of Mod_subst are horrendous as they rely on physical equality (!) for some reason, resulting in interesting eisenbugs while trying to change the implementation.

Fixes #22426: Self-equivalence within δ-resolvers not stable by aliasing.

[ppedrot]

Note that the example added after the fact in #22426 is not solved by this patch, so I'll put it in a different issue.

[SkySkimmer]

@coqbot merge now