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 y ∈ Y.

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 Hy1: (x,y) 1 ∈ Y.

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

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

An exact proof term for the current goal is Hy1.

∎