Mentions légales du service
At this commit and before, pure Hoare-style reasoning is based on simp and so is restricted to confluent computations.
