Commit 2023-10-16 08:03 7e8b89e3

fix: add missing DecidableEq arguments (#7702) These make the lemmas strictly more (syntactically) general. As usual, the way to find these is to remove open Classical and fix what breaks. Usually this means adding classical to the start of the proof, but there are lots of weird term-mode proofs here for which adding a more surgical letI := Classical.decEq is easier.