Commit 2025-01-15 15:41 739d7770

refactor: redefine Subrel in terms of α → Prop instead of Set α (#20475) Currently, Subrel r {x | p x} interacts poorly with simp, as the type signature is rewritten from ↑{x | p x} → ↑{x | p x} → Prop to {x // p x} → {x // p x} → Prop. This can be avoided by writing Subrel r p instead.