Let x be given.

Assume Hx.

We will prove pa (conj (proj0 x)) (- proj1 x) = conj 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 (conj x) 0 = conj x.

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

∎