Improve diverges effect

This is an attempt at implementing #184 (closed).

The second commit also forbids to instantiate a symbol by another symbol with worse termination status (in master, instantiating a non-divergent symbol by a divergent one generates a "false" VC but still typechecks).