Let X and Y be given.

Apply set_ext to the current goal.

We will prove proj0 (pair X Y) ⊆ X.

Let u be given.

Assume H1: u ∈ proj0 (pair X Y).

We will prove u ∈ X.

Apply (pairE0 X Y u) to the current goal.

We will prove pair 0 u ∈ pair X Y.

An exact proof term for the current goal is (proj0E (pair X Y) u H1).

We will prove X ⊆ proj0 (pair X Y).

Let u be given.

Assume H1: u ∈ X.

We will prove u ∈ proj0 (pair X Y).

Apply proj0I to the current goal.

We will prove pair 0 u ∈ pair X Y.

Apply pairI0 to the current goal.

We will prove u ∈ X.

An exact proof term for the current goal is H1.

∎