Let z and w be given.

Assume Hz Hw.

We will prove CD_carr (pa (proj0 z + proj0 w) (proj1 z + proj1 w)).

Apply CD_carr_I to the current goal.

Apply F_add to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hw.

Apply F_add to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hw.

∎