Allow swapping later^i and forall, later, etc.
For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR). For swapping later^i and later, I'm not sure what's the typeclass, but it should be possible — I do the swaps through complicated proofs, applied inline.
Generally, I suspect all the instances for later could be lifted (by induction) to later^i, and I suspect I'd be willing to do that work (once I move).