Framing: Make* classes lead to suboptimal results
Make* classes to turn terms into a certain form, e.g. a leading
▷^n. However, those classes require the original term to be equivalent with the converted one. This leads to situations such as
Lemma test_iFrame_later_rel (P : PROP) : ▷ P -∗ (▷ (P ∧ P)). Proof. iIntros "?". iFrame. (* Now the goal is [▷ emp] *)
I would expect the goal to become
emp (and hence
iFrame closing the goal), and indeed that would be sound (
▷ emp) but it doesn't happen.