Let x and y be given.

Assume Hx Hy.

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

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

Assume H2: ∃y', F y' ∧ pa x y = pa (proj0 (pa x y)) y'.

Apply H2 to the current goal.

Let y' be given.

Assume H3.

Apply H3 to the current goal.

Assume Hy': F y'.

Assume H4: pa x y = pa (proj0 (pa x y)) y'.

Use symmetry.

An exact proof term for the current goal is pair_tag_prop_1 x y (proj0 (pa x y)) y' Hx H1 H4.

∎