Let x and y be given.

We will prove pair (pair x y 0) (pair x y 1) = pair x y.

rewrite the current goal using pair_ap_0 (from left to right).

rewrite the current goal using pair_ap_1 (from left to right).

Use reflexivity.

∎