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.