Also, make the setup of IntoLaterN more consistent with that of WandWeaken.
Maybe, we should do something similar for other proof mode classes too.