Give names to ensures and invariant
This MR allows naming ensures and invariant when they appear as hypotheses.
Naming assert and requires was resolved by !129 (merged). Naming returns and 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)