Let x and y be given.

Assume Hx Hy.

Use symmetry.

Apply CD_proj1_1 (pa x y) (CD_carr_I x y Hx Hy) to the current goal.

Assume H1: F (proj1 (pa x y)).

Apply CD_proj0_2 x y Hx Hy (λu v ⇒ pa x y = pa v (proj1 (pa x y)) → y = proj1 (pa x y)) to the current goal.

Assume H2: pa x y = pa x (proj1 (pa x y)).

An exact proof term for the current goal is pair_tag_prop_2 x y x (proj1 (pa x y)) Hx Hy Hx H1 H2.

∎