Strong persistent framing and saved_prop_agree
If I have in my persistent context
Hx: saved_prop_own γ xand
Hy: saved_prop_own γ y, then
iDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"gives
x = x. To get the right result, instead I need to instantiate
saved_prop_agree _ x y, which is less convenient.