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.