Commit 2026-06-17 15:42 e1d1de3b
View on Github →feat(Convert): less aggressive congruence (#38071)
This PR tries to make convert behave more predictably, disabling some of the aggressive congruence steps that congr! does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications.