Strong persistent framing and saved_prop_agree
Problem reported by @haidang in #71 (closed):
If I have in my persistent context
Hx: saved_prop_own γ x
andHy: saved_prop_own γ y
, theniDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"
givesx = x
. To get the right result, instead I need to instantiatesaved_prop_agree _ x y
, which is less convenient.