this makes it slightlymore annoying to use because we have to elliminate the box. one more reason to have a proof mode ;-)