Reconsider normalizing `/\ emp` into `<affine>`
I was rather surprised when running iFrame
added an <affine>
modality in front of a goal. @robbertkrebbers explained:
To understand what's happening, first note that when you frame something in a general BI, it will turn it into
emp
, notTrue
. So, framing let's sayP
inP ∗ Q
turns it intoemp ∗ Q
, which then get beautified intoQ
.
In this case, you are framing
P
in<pers> Q ∧ P
, which will turn it into<pers> Q ∧ emp
. This is then beautified into<affine> <pers> Q
I think we should not perform this normalization, and just keep it as <pers> Q /\ emp
.