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.