We will prove (∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, ((λx y : set ⇒ (x,y)) x y) ∈ λx ∈ X ⇒ F x).

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

An exact proof term for the current goal is lamI.

∎