Let X, Y and y be given.

Assume H1: pair 1 y ∈ pair X Y.

We will prove y ∈ Y.

Apply (pairE X Y (pair 1 y) H1) to the current goal.

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

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

Assume H2: ∃x ∈ X, Inj1 y = Inj0 x.

We will prove False.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ Inj1 y = Inj0 x) H2) to the current goal.

Let x be given.

Assume _.

Assume H3: Inj1 y = Inj0 x.

Apply (Inj0_Inj1_neq x y) to the current goal.

Use symmetry.

An exact proof term for the current goal is H3.

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

Assume H2: ∃y' ∈ Y, Inj1 y = Inj1 y'.

Apply (exandE_i (λy' ⇒ y' ∈ Y) (λy' ⇒ Inj1 y = Inj1 y') H2) to the current goal.

Let y' be given.

Assume H3: y' ∈ Y.

Assume H4: Inj1 y = Inj1 y'.

We will prove y ∈ Y.

rewrite the current goal using (Inj1_inj y y' H4) (from left to right).

We will prove y' ∈ Y.

An exact proof term for the current goal is H3.

∎