Let X, Y and z be given.

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

We prove the intermediate claim L1: ∃x ∈ X, z ∈ {pair x y|y ∈ Y x}.

An exact proof term for the current goal is (famunionE X (λx ⇒ {pair x y|y ∈ Y x}) z H1).

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z ∈ {pair x y|y ∈ Y x}) L1) to the current goal.

Let x be given.

Assume H2: x ∈ X.

Assume H3: z ∈ {pair x y|y ∈ Y x}.

Apply (ReplE_impred (Y x) (pair x) z H3) to the current goal.

Let y be given.

Assume H4: y ∈ Y x.

Assume H5: z = pair x y.

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

We will prove pair (proj0 (pair x y)) (proj1 (pair x y)) = pair x y ∧ proj0 (pair x y) ∈ X ∧ proj1 (pair x y) ∈ Y (proj0 (pair x y)).

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

We will prove pair x (proj1 (pair x y)) = pair x y ∧ x ∈ X ∧ proj1 (pair x y) ∈ Y x.

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

We will prove pair x y = pair x y ∧ x ∈ X ∧ y ∈ Y x.

Apply and3I to the current goal.

We will prove pair x y = pair x y.

Use reflexivity.

We will prove x ∈ X.

An exact proof term for the current goal is H2.

We will prove y ∈ Y x.

An exact proof term for the current goal is H4.

∎