We will prove ∀u ∈ (λx ∈ X ⇒ F x), pair_p u ∧ u 0 ∈ X.

Let u be given.

Assume Hu: u ∈ λx ∈ X ⇒ F x.

We prove the intermediate claim L1: ∃x ∈ X, ∃y ∈ F x, u = pair x y.

An exact proof term for the current goal is (lamE X F u Hu).

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ ∃y ∈ F x, u = pair x y) L1) to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume H2: ∃y ∈ F x, u = pair x y.

Apply (exandE_i (λy ⇒ y ∈ F x) (λy ⇒ u = pair x y) H2) to the current goal.

Let y be given.

Assume Hy: y ∈ F x.

Assume H3: u = pair x y.

Apply andI to the current goal.

We will prove pair_p u.

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

Apply pair_p_I to the current goal.

We will prove u 0 ∈ X.

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

We will prove pair x y 0 ∈ X.

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

We will prove x ∈ X.

An exact proof term for the current goal is Hx.

We will prove ∀x ∈ X, (λx ∈ X ⇒ F x) x ∈ Y x.

Let x be given.

Assume Hx: x ∈ X.

rewrite the current goal using (beta X F x Hx) (from left to right).

We will prove F x ∈ Y x.

An exact proof term for the current goal is (H1 x Hx).