# 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"`

.