Reformat mwhile_exists proof (see 52ac2c6) to make it fit in < 80 cols.