Rewrite unexpectedly failing (Nested below |-, *, \later, -*)
The rewrite at https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66 is unexpectedly failing.
The goal is of the shape
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
and I am trying to rewrite backwards with P ⊢ |={E}=> P
to remove the fancy update (behind the linear view shift notation).
Cc @robbertkrebbers could you have a look at this?