PR #11303: refactor(order/well_founded_set): golf, review...

Stream: triage

[Random Issue Bot]

Today I chose PR 11303 for discussion!

refactor(order/well_founded_set): golf, review API
Created by @Yury G. Kudryashov (@urkud) on 2022-01-07
Labels: delegated, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Can fix it easily. It's just that a theorem got added in the meantime and I went onto generalizing it but I couldn't.

[Eric Wieser]

This one has picked up conflicts again