Commit 2026-06-02 07:58 6933418b
View on Github →feat: x ∈ s ⇨ t ↔ x ∈ s → x ∈ t (for finsets) (#40140)
I was too hasty in sending #40133 to bors, sorry!
This PR also renames mem_bihimp → mem_bihimp_iff without deprecation (it landed only a few hours ago).