Commit 2025-11-24 07:57 0f04a8f3

View on Github →

feat: make sure that simp computes {a} ∩ s (#31947) These simp lemmas were missing for simp to be able to compute {a} ∩ s depending on whether a is in s or not.

Estimated changes