Let X, Y and z be given.

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

Apply proj0_Sigma to the current goal.

∎