Let z be given.

Assume Hz.

We will prove CD_carr (pa (conj (proj0 z)) (- proj1 z)).

Apply CD_carr_I to the current goal.

Apply F_conj to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_minus to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

∎