Improve provability of the View service set
Cleanup the B specifications of the modules below service_set_view
to make them provable (mostly by removing what is clearly incorrect or not corresponding to the implementation).
To be continued in #1152 (closed).
Edited by Vincent Monfort