Let x and y be given.

Assume Hx Hy.

We will prove pa (proj0 x + proj0 y) (proj1 x + proj1 y) = x + y.

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 CD_proj0_F F_0 y Hy (from left to right).

rewrite the current goal using CD_proj1_F F_0 y Hy (from left to right).

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

We will prove pa (x + y) 0 = x + y.

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

∎