Let x and y be given.

Assume Hx Hy.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv Huv.

Apply set_ext to the current goal.

An exact proof term for the current goal is ctagged_eqE_Subq x y Hx u Hu v Huv.

Apply ctagged_eqE_Subq y x Hy v Hv u to the current goal.

Use symmetry.

An exact proof term for the current goal is Huv.

∎