Apply a view to the n top assumptions

[fdupress]

Consider a lemma of the form H: forall x, P x => Q x => R x and a goal of the form P y => Q y => T y.

I would like to be able to apply H as a view to P y and Q y in one go, so that move=> /H (with suitable syntax) leaves goal R y => T y.

One syntax (riffing off the recent extension on including intro-patterns in proof terms) could be move=> (H _ ^ ^). This would then enable a mix of instantiation and deferral for view hypotheses. [^2], for example, could be used to reorder top assumptions when applying the view.

Most of this can (probably) be implemented internally as introducing select top assumptions and constructing the proof term to apply as a view.