It also suggests (and I'm surprised I didn't think of it before) that perhaps there ought to be a constructive dual to the proof irrelevant modality --- not the "intentisonal" dual to the concept of proof irrelevance in the sense of Pfenning '01, but something that has the same demote/promote sort of protocol, but on opposite sides of the turnstile.
But it would be rather degenerate for the same reason as the classical (nonlinear) dual would be, so maybe it makes more sense linearly, too...
