Let X, Y and z be given.

Assume H1: z ∈ ∑x ∈ X, Y x.

Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z ∈ X) (proj1 z ∈ Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.

Assume _ H2 _.

An exact proof term for the current goal is H2.

∎