Faster reduction engine in the kernel

[leodemoura]

We have only one reduction strategy when checking definitional equality in the kernel. It uses the "lazy unfolding" and it is suboptimal for many applications. Examples:

• Any application that makes heavy use of "proof` by reflection"
• Any application that has to check many ground terms are definitionally equal or not. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Performance.20issues.20with.20big.20case.20split