Scheme Equality depends on the size of the fully reduced type when it should not #16290
Description
Ah! Told you so. I have a partially written fix for this though, I can push it somewhere after some polishing.
@ppedrot Should we open a separate issue to track this?
I've pushed an update to mit-plv/fiat-crypto#1293 disabling the equality generation and I've restarted the CI here. I've also opened rocq-community/coq-performance-tests#22 with the smaller examples
Originally posted by @JasonGross in #16206 (comment)
Variant of #16172 to track the issue in Scheme Equality