Have iNext "pull" laters out from below other operators.
Let's say I have a goal of the shape
∃ x, ▷ Q x (and the type of
x is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to
▷ ∃ x, Q x. Currently, I have to do
rewrite -uPred.later_exist for this.
First of all, I am wondering why
iApply uPred.later_exist doesn't work in this context. Secondly, it'd be nice if
iNext could also "pull" laters out of the goal if there's not yet a top-level later.