Let x and y be given.

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

We will prove proj1 (pair x y) = y.

Apply proj1_pair_eq to the current goal.

∎