Let x and y be given.

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

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

Apply proj0_pair_eq to the current goal.

∎