Moving hypotheses from the intuitionistic to the spatial context
Right now, there appears to be no decent way to move hypotheses from the intuitionistic context to the spatial context.
I thought this should never be needed, but I was proved wrong. As @jtassaro shows in (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/171/diffs#d026f8137ab7b7e373742e0df76ccf325011a5cf_53_89), this is sometimes needed before doing an induction.
I suppose we could make a tactic for this (and a corresponding introduction pattern like -# pat), but I'm not sure I like that very much. Also, in the case of a generic BI, there is probably the choice of having an <affine> modality or not.
As an alternative, if we believe this only ever occurs when doing induction, we could extend the syntax of the forall argument of iInduction to allow moving hypotheses from the intuitionistic to the spatial context.