Introduce implication if premise is persistent
Currently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the goal is box P -> Q, introducing should be possible even for a non-empty spatial context.