Add introduction pattern `-# pat` to move a hypothesis to the spatial context

This MR fixes #213 (closed)

Rationale: When porting @msammler's development to !341 (merged), the result H of an iAssert P as "H" ended up in the intuitionistic instead of spatial context. While this desirable most of the time (since no hypotheses are used to prove P, we can assume that P holds intuitionistically), it may be too strong if one wants to do an induction. The -# introduction pattern can thus be used to move the result to the spatial context. For @msammler's example, one can thus write iAssert P as "-#H".