iMod: Control which modality is reduced
The following proof script should work, but does not
Lemma test_iModElim_box P : □ P -∗ P.
Proof. iIntros ">H". iAssumption. Qed.
The following proof script should work, but does not
Lemma test_iModElim_box P : □ P -∗ P.
Proof. iIntros ">H". iAssumption. Qed.