Let u be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ proj1 u.

We will prove w ∈ u 1.

Apply apI to the current goal.

We will prove pair 1 w ∈ u.

Apply proj1E to the current goal.

We will prove w ∈ proj1 u.

An exact proof term for the current goal is H1.

Let w be given.

Assume H1: w ∈ u 1.

We will prove w ∈ proj1 u.

Apply proj1I to the current goal.

We will prove pair 1 w ∈ u.

Apply apE to the current goal.

We will prove w ∈ u 1.

An exact proof term for the current goal is H1.

∎