Make `whnf()` less agressive

Right now, whnf() returns a weak-head normal form as expected, but it normalizes the terms too much, leading to some branches of the conversion checker being unused and useless, the function needs further investigation to ensure it only normalizes as much as needed.