Reduce projections during unification#20730

Tragicus wants to merge 2 commits into

rocq-prover:masterrocq-prover/rocq:masterfrom

Tragicus:reduce-projsTragicus/coq:reduce-projsCopy head branch name to clipboard