Let x be given.

Assume Hx.

We will prove pa (- proj0 x) (- proj1 x) = - x.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

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

We will prove pa (- x) 0 = - x.

An exact proof term for the current goal is pair_tag_0 (- x).

∎