Let x and y be given.

We will prove (x,y) 1 = y.

rewrite the current goal using (tuple_pair x y) (from right to left).

An exact proof term for the current goal is (pair_ap_1 x y).

∎