Let f, X and Y be given.

Assume Hsub: f ⊆ setprod X Y.

Let x and y be given.

Assume Hxy: (x,y) ∈ f.

We will prove x ∈ X.

We prove the intermediate claim HxyXY: (x,y) ∈ setprod X Y.

An exact proof term for the current goal is (Hsub (x,y) Hxy).

We prove the intermediate claim Hx0: (x,y) 0 ∈ X.

An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) (x,y) HxyXY).

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

An exact proof term for the current goal is Hx0.

∎