Last two explicit arguments

Stream: lean4

[Siddhartha Gadgil]

Is there a quick way to decompose a relation application to get the last two explicit arguments, i.e., which acts as the solution to

z ← mpAppM' r #[x, y]

where z is known and we want r, x and y?

This is for repairing trans, one of whose failure cases is caused by @HEq: {α : Sort u_1} → α → {β : Sort u_1} → β → Prop. The present code naively assumes that x and y are the last two arguments.

It seems that a meta-telescope giving binders should do this smoothly, but I am not used to using these.