Let u be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ proj0 u.

We will prove w ∈ u 0.

Apply apI to the current goal.

We will prove pair 0 w ∈ u.

Apply proj0E to the current goal.

We will prove w ∈ proj0 u.

An exact proof term for the current goal is H1.

Let w be given.

Assume H1: w ∈ u 0.

We will prove w ∈ proj0 u.

Apply proj0I to the current goal.

We will prove pair 0 w ∈ u.

Apply apE to the current goal.

We will prove w ∈ u 0.

An exact proof term for the current goal is H1.

∎