Let X, Y and p be given.

Assume Hp: p ∈ setprod X Y.

We will prove p = (p 0,p 1).

Apply (Sigma_E X (λ_ : set ⇒ Y) p Hp) to the current goal.

Let x be given.

Assume Hx_pair.

Apply Hx_pair to the current goal.

Assume HxX Hexy.

Apply Hexy to the current goal.

Let y be given.

Assume Hy_pair.

Apply Hy_pair to the current goal.

Assume HyY Hpeq.

We prove the intermediate claim HeqT: p = (x,y).

We will prove p = (x,y).

rewrite the current goal using (tuple_pair x y) (from right to left).

An exact proof term for the current goal is Hpeq.

We prove the intermediate claim Hp0: p 0 = x.

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

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

We prove the intermediate claim Hp1: p 1 = y.

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

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

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

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

An exact proof term for the current goal is HeqT.

∎