This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does
not immediately close the goal by reflexivity.