Commit 2025-11-20 19:06 2100ab26

fix(rw??): whnf on equality hypotheses (#31609) This PR adds some missing whnf in the rw?? implementation. This only affects the behaviour of rewriting with local variables. I discovered that sometimes the type can be an uninstantiated metavariable that needs to first instantiated, for example by using whnf.