iMod should be able to eliminate <pers> and <plain> in the intuitionistic context

With an assumption H: ■ P in the intuitionistic context, I was wondering how I can eliminate that modality. Doing so relies on the fact that the intuitionistic context is affine, so this can't be done by just applying a lemma. Then I realized that iMod is what we use to eliminate modalities -- but it doesn't work here: I am told that iMod cannot eliminate this modality.

I suppose adding the right typeclass instances should fix this?