First try in this normalization process.

Several cleaning ideas:

1) Avoid side effects on instances as much as possible. The general
goal is that the presence/absence and the order of "Require Import"
should not break a development too easily.

2) Have systematic header (that we can generate automatically) for
each "model setting" wrt synchronicity, topology, felxibility,
observation, etc.

Strategy:
- avoiding Require Export.

- avoiding Import as much as possible. Only very generic definitions
  are allowed to be imported (Require is of course allowed). Reason:
  it also imports Non Local Instances and notations.
  We may swithc to Local Instance and Local Notation instead, and
  allow more imports later.

- avoid Global Instances as much as possible.