Let X, Y and f be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1 _ H2.
We will prove (uX, f u Y) (wY, uX, f u = w).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.