An exact proof term for the current goal is λX Y x Hx y Hy ⇒ tuple_2_Sigma X (λ_ ⇒ Y) x Hx y Hy.