Let U, V, X and Y be given.

Assume HU: U ⊆ X.

Assume HV: V ⊆ Y.

We will prove setprod U V ⊆ setprod X Y.

Let p be given.

Assume Hp: p ∈ setprod U V.

We will prove p ∈ setprod X Y.

We prove the intermediate claim Hp0: p 0 ∈ U.

An exact proof term for the current goal is (ap0_Sigma U (λu ⇒ V) p Hp).

We prove the intermediate claim Hp1: p 1 ∈ V.

An exact proof term for the current goal is (ap1_Sigma U (λu ⇒ V) p Hp).

We prove the intermediate claim Hp0X: p 0 ∈ X.

An exact proof term for the current goal is (HU (p 0) Hp0).

We prove the intermediate claim Hp1Y: p 1 ∈ Y.

An exact proof term for the current goal is (HV (p 1) Hp1).

We prove the intermediate claim Heta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta U V p Hp).

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

We will prove (p 0,p 1) ∈ setprod X Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (p 0) (p 1) Hp0X Hp1Y).

∎