Make iSplit work below existentials?
I have a goal of the form
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
and all my assumptions are only available later. I cannot do
iNext because not everything is below a later, but I can do
rewrite -uPred.sep_exist_l. iSplit; first done.. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for
iSplit to work in this case (giving me
⌜#l = #l⌝ and
∃ x : vec val m, ▷ l ↦∗ x as goals)? The rewrite I did above is not very discoverable, but neither is the
iSplit. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form
∃ x y z, P work much better with the proofmode, because I an do a single
iDestruct ... as (x y z) .... If I pushed the existential down, destructing things would become much more annoying.)