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?