Give names to ensures and invariant
This MR allows naming
invariant when they appear as hypotheses.
requires was resolved by !129 (merged). Naming
raises is omitted for now, because it is unclear how the name relates to the different cases.
variant never appears as precondion.
Closes #261 (closed)