Let X, Y and z be given.

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

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

Apply proj1_Sigma to the current goal.

∎