Let x, y, U, V and p be given.
Assume Hpxy: p ∈ setprod {x} {y}.
Assume HpUV: p ∈ setprod U V.
We will prove x ∈ U ∧ y ∈ V.
We prove the intermediate claim Hp0x: p 0 ∈ {x}.
An exact proof term for the current goal is (ap0_Sigma {x} (λu ⇒ {y}) p Hpxy).
We prove the intermediate claim Hp1y: p 1 ∈ {y}.
An exact proof term for the current goal is (ap1_Sigma {x} (λu ⇒ {y}) p Hpxy).
We prove the intermediate claim Hp0_eq_x: p 0 = x.
An exact proof term for the current goal is (singleton_elem (p 0) x Hp0x).
We prove the intermediate claim Hp1_eq_y: p 1 = y.
An exact proof term for the current goal is (singleton_elem (p 1) y Hp1y).
We prove the intermediate claim Hp0U: p 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λu ⇒ V) p HpUV).
We prove the intermediate claim Hp1V: p 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λu ⇒ V) p HpUV).
Apply andI to the current goal.
We will prove x ∈ U.
rewrite the current goal using Hp0_eq_x (from right to left).
An exact proof term for the current goal is Hp0U.
We will prove y ∈ V.
rewrite the current goal using Hp1_eq_y (from right to left).
An exact proof term for the current goal is Hp1V.
∎