replaced the 'variant {0}' by diverges to avoid unproved goals
but now we have warnings.

TO INVESTIGATE: uncomment the commented variants, that are supposed to work