Assume H0.

Let x be given.

Assume Hx.

rewrite the current goal using pair_tag_0 x (from right to left) at position 1.

We will prove CD_proj1 (pair_tag x 0) = 0.

An exact proof term for the current goal is CD_proj1_2 x 0 Hx H0.

∎