Let X, Y and z be given.

Assume Hz: 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 Hz)) to the current goal.

Assume H1: pair (proj0 z) (proj1 z) = z.

Assume H2: proj0 z ∈ X.

Assume H3: proj1 z ∈ Y (proj0 z).

We use (proj0 z) to witness the existential quantifier.

Apply andI to the current goal.

We will prove proj0 z ∈ X.

An exact proof term for the current goal is H2.

We use (proj1 z) to witness the existential quantifier.

Apply andI to the current goal.

We will prove proj1 z ∈ Y (proj0 z).

An exact proof term for the current goal is H3.

We will prove z = pair (proj0 z) (proj1 z).

Use symmetry.

An exact proof term for the current goal is H1.

∎