Framing persistent hypotheses under a later in the goal
I have
"H": P
-------------□
▷ P ∗ Q
iFrame "H"
gives me back ▷ emp ∗ Q
. I was working with an affine BI.
@jtassaro suggests to generalize make_sep_emp_l
.
I have
"H": P
-------------□
▷ P ∗ Q
iFrame "H"
gives me back ▷ emp ∗ Q
. I was working with an affine BI.
@jtassaro suggests to generalize make_sep_emp_l
.