Commit 2024-03-21 23:59 eb5cb7e4

feat: let congr! discharge equalities of BEq instances (#11179) Adds a congruence lemma for BEq instances that makes use of LawfulBEq instances, and gives congr! the ability to use this congruence lemma. This is meant to help with diamonds that arise from interactions between Decidable and BEq instances. This feature can be turned off using the beqEq configuration setting, like congr! (config := { beqEq := false }).