Let X, Y and x be given.
Assume H1: pair 0 x ∈ pair X Y.
We will prove x ∈ X.
Apply (pairE X Y (pair 0 x) H1) to the current goal.
rewrite the current goal using Inj0_pair_0_eq (from right to left).
Assume H2: ∃x' ∈ X, Inj0 x = Inj0 x'.
Apply (exandE_i (λx' ⇒ x' ∈ X) (λx' ⇒ Inj0 x = Inj0 x') H2) to the current goal.
Let x' be given.
Assume H3: x' ∈ X.
Assume H4: Inj0 x = Inj0 x'.
We will prove x ∈ X.
rewrite the current goal using (Inj0_inj x x' H4) (from left to right).
We will prove x' ∈ X.
An exact proof term for the current goal is H3.
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: ∃y ∈ Y, Inj0 x = Inj1 y.
We will prove False.
Apply (exandE_i (λy ⇒ y ∈ Y) (λy ⇒ Inj0 x = Inj1 y) H2) to the current goal.
Let y be given.
Assume _.
Assume H3: Inj0 x = Inj1 y.
An exact proof term for the current goal is (Inj0_Inj1_neq x y H3).
∎