Let x and y be given.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z pair x y.
Apply (pairE x y z Hz) to the current goal.
Assume H1: ux, z = pair 0 u.
Apply (exandE_i (λu ⇒ u x) (λu ⇒ z = pair 0 u) H1) to the current goal.
Let u be given.
Assume Hu: u x.
Assume H2: z = pair 0 u.
We will prove z (x,y).
We will prove z λi2 if i = 0 then x else y.
rewrite the current goal using H2 (from left to right).
We will prove pair 0 u λi2 if i = 0 then x else y.
Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 0 In_0_2 u) to the current goal.
We will prove u if 0 = 0 then x else y.
rewrite the current goal using (If_i_1 (0 = 0) x y (λq H ⇒ H)) (from left to right).
We will prove u x.
An exact proof term for the current goal is Hu.
Assume H1: uy, z = pair 1 u.
Apply (exandE_i (λu ⇒ u y) (λu ⇒ z = pair 1 u) H1) to the current goal.
Let u be given.
Assume Hu: u y.
Assume H2: z = pair 1 u.
We will prove z (x,y).
We will prove z λi2 if i = 0 then x else y.
rewrite the current goal using H2 (from left to right).
We will prove pair 1 u λi2 if i = 0 then x else y.
Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 1 In_1_2 u) to the current goal.
We will prove u if 1 = 0 then x else y.
rewrite the current goal using (If_i_0 (1 = 0) x y neq_1_0) (from left to right).
We will prove u y.
An exact proof term for the current goal is Hu.
Let z be given.
Assume Hz: z (x,y).
We will prove z pair x y.
We prove the intermediate claim L1: i2, w(if i = 0 then x else y), z = pair i w.
An exact proof term for the current goal is (lamE 2 (λi ⇒ if i = 0 then x else y) z Hz).
Apply (exandE_i (λi ⇒ i 2) (λi ⇒ w(if i = 0 then x else y), z = pair i w) L1) to the current goal.
Let i be given.
Assume Hi: i 2.
Assume H1: w(if i = 0 then x else y), z = pair i w.
Apply (exandE_i (λw ⇒ w if i = 0 then x else y) (λw ⇒ z = pair i w) H1) to the current goal.
Let w be given.
Assume Hw: w if i = 0 then x else y.
Assume H2: z = pair i w.
We will prove z pair x y.
rewrite the current goal using H2 (from left to right).
We will prove pair i w pair x y.
We prove the intermediate claim L2: i {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 i Hi).
Apply (UPairE i 0 1 L2) to the current goal.
Assume Hi0: i = 0.
rewrite the current goal using Hi0 (from left to right).
We will prove pair 0 w pair x y.
Apply pairI0 to the current goal.
We will prove w x.
We prove the intermediate claim L3: (if i = 0 then x else y) = x.
An exact proof term for the current goal is (If_i_1 (i = 0) x y Hi0).
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw.
Assume Hi1: i = 1.
rewrite the current goal using Hi1 (from left to right).
We will prove pair 1 w pair x y.
Apply pairI1 to the current goal.
We will prove w y.
We prove the intermediate claim L3: (if i = 0 then x else y) = y.
rewrite the current goal using Hi1 (from left to right).
An exact proof term for the current goal is (If_i_0 (1 = 0) x y neq_1_0).
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw.