Commit 2025-02-03 07:17 da0385c6
View on Github →chore(Logic/Equiv): change type of sumEquivSigmaBool to simp normal form (#21338)
simp eagerly rewrites Bool.casesOn to Bool.rec, so using the former in the type signature prevents related simp lemmas from firing.
See Zulip discussion.